1 /-
2 Copyright (c) 2019 Johan Commelin. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johan Commelin, Kenny Lau
5 -/
6
7 import data.finsupp order.complete_lattice algebra.ordered_group data.mv_polynomial
src └──────────┘ └────────────────────┘ └───────────────────┘ └────────────────┘
8 import algebra.order_functions
src └─────────────────────┘
9 import ring_theory.ideal_operations
src └──────────────────────────┘
10
11 /-!
12 # Formal power series
13
14 This file defines (multivariate) formal power series
15 and develops the basic properties of these objects.
16
17 A formal power series is to a polynomial like an infinite sum is to a finite sum.
18
19 We provide the natural inclusion from polynomials to formal power series.
20
21 ## Generalities
22
23 The file starts with setting up the (semi)ring structure on multivariate power series.
24
25 `trunc n φ` truncates a formal power series to the polynomial
26 that has the same coefficients as φ, for all m ≤ n, and 0 otherwise.
27
28 If the constant coefficient of a formal power series is invertible,
29 then this formal power series is invertible.
30
31 Formal power series over a local ring form a local ring.
32
33 ## Formal power series in one variable
34
35 We prove that if the ring of coefficients is an integral domain,
36 then formal power series in one variable form an integral domain.
37
38 The `order` of a formal power series `φ` is the multiplicity of the variable `X` in `φ`.
39
40 If the coefficients form an integral domain, then `order` is a valuation
41 (`order_mul`, `order_add_ge`).
42
43 ## Implementation notes
44
45 In this file we define multivariate formal power series with
46 variables indexed by `σ` and coefficients in `α` as
47 mv_power_series σ α := (σ →₀ ℕ) → α.
48 Unfortunately there is not yet enough API to show that they are the completion
49 of the ring of multivariate polynomials. However, we provide most of the infrastructure
50 that is needed to do this. Once I-adic completion (topological or algebraic) is available
51 it should not be hard to fill in the details.
52
53 Formal power series in one variable are defined as
54 power_series α := mv_power_series unit α.
55
56 This allows us to port a lot of proofs and properties
57 from the multivariate case to the single variable case.
58 However, it means that formal power series are indexed by (unit →₀ ℕ),
59 which is of course canonically isomorphic to ℕ.
60 We then build some glue to treat formal power series as if they are indexed by ℕ.
61 Occasionally this leads to proofs that are uglier than expected.
62
63 -/
64
65 noncomputable theory
66 open_locale classical
67
68 /-- Multivariate formal power series, where `σ` is the index set of the variables
69 and `α` is the coefficient ring.-/
70 def mv_power_series (σ : Type*) (α : Type*) := (σ →₀ ℕ) → α
id ┴ └┘ ┴ ┴
src └┘ ┴
typ ┴ └┘ ┴ ┴
doc └┘
71
72 namespace mv_power_series
73 open finsupp
74 variables {σ : Type*} {α : Type*}
75
76 instance [inhabited α] : inhabited (mv_power_series σ α) := ⟨λ _, default _⟩
id └───────┘ ┴ └───────┘ └─────────────┘ ┴ ┴ ┴ └─────┘
src └───────┘ └───────┘ └─────────────┘ └─────┘
typ └───────┘ ┴ └───────┘ └─────────────┘ ┴ ┴ ┴ └─────┘
doc └─────────────┘
77 instance [has_zero α] : has_zero (mv_power_series σ α) := pi.has_zero
id └──────┘ ┴ └──────┘ └─────────────┘ ┴ ┴ └─────────┘
src └──────┘ └──────┘ └─────────────┘ └─────────┘
typ └──────┘ ┴ └──────┘ └─────────────┘ ┴ ┴ └─────────┘
doc └─────────────┘
78 instance [add_monoid α] : add_monoid (mv_power_series σ α) := pi.add_monoid
id └────────┘ ┴ └────────┘ └─────────────┘ ┴ ┴ └───────────┘
src └────────┘ └────────┘ └─────────────┘ └───────────┘
typ └────────┘ ┴ └────────┘ └─────────────┘ ┴ ┴ └───────────┘
doc └─────────────┘
79 instance [add_group α] : add_group (mv_power_series σ α) := pi.add_group
id └───────┘ ┴ └───────┘ └─────────────┘ ┴ ┴ └──────────┘
src └───────┘ └───────┘ └─────────────┘ └──────────┘
typ └───────┘ ┴ └───────┘ └─────────────┘ ┴ ┴ └──────────┘
doc └─────────────┘
80 instance [add_comm_monoid α] : add_comm_monoid (mv_power_series σ α) := pi.add_comm_monoid
id └─────────────┘ ┴ └─────────────┘ └─────────────┘ ┴ ┴ └────────────────┘
src └─────────────┘ └─────────────┘ └─────────────┘ └────────────────┘
typ └─────────────┘ ┴ └─────────────┘ └─────────────┘ ┴ ┴ └────────────────┘
doc └─────────────┘
81 instance [add_comm_group α] : add_comm_group (mv_power_series σ α) := pi.add_comm_group
id └────────────┘ ┴ └────────────┘ └─────────────┘ ┴ ┴ └───────────────┘
src └────────────┘ └────────────┘ └─────────────┘ └───────────────┘
typ └────────────┘ ┴ └────────────┘ └─────────────┘ ┴ ┴ └───────────────┘
doc └─────────────┘
82
83 section add_monoid
84 variables [add_monoid α]
id └────────┘
src └────────┘
typ └────────┘
85
86 variables (α)
87
88 /-- The `n`th monomial with coefficient `a` as multivariate formal power series.-/
89 def monomial (n : σ →₀ ℕ) : α →+ mv_power_series σ α :=
id ┴ └┘ ┴ ┴ └┘ └─────────────┘ ┴ ┴
src └┘ ┴ └┘ └─────────────┘
typ ┴ └┘ ┴ ┴ └┘ └─────────────┘ ┴ ┴
doc └┘ └┘ └─────────────┘
90 { to_fun := λ a m, if m = n then a else 0,
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
91 map_zero' := funext $ λ m, by { split_ifs; refl },
id └────┘ ┴
src └────┘ └───────┘ └───┘
typ └────┘ ┴ └───────┘ └───┘
doc └───────┘ └───┘
txt └───────┘ └───┘
par └───────┘ └───┘
pid ┴
st └─────────────────┘└┘
92 map_add' := λ a b, funext $ λ m,
id ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ └────┘ ┴
93 show (if m = n then a + b else 0) = (if m = n then a else 0) + (if m = n then b else 0),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
94 from if h : m = n then by simp only [if_pos h] else by simp only [if_neg h, add_zero] }
id └┘ ┴ ┴ ┴ └────┘ ┴ └────┘ ┴ └──────┘
src └┘ ┴ └─────────┘└────┘┴ └┘ └─────────┘└────┘┴ └┘└──────┘└┘
typ └┘ ┴ ┴ ┴ └─────────┘└────┘┴┴└┘ └─────────┘└────┘┴┴└┘└──────┘└┘
doc └─────────┘ ┴ └┘ └─────────┘ ┴ └┘ └┘
txt └─────────┘ ┴ └┘ └─────────┘ ┴ └┘ └┘
par └─────────┘ ┴ └┘ └─────────┘ ┴ └┘ └┘
pid ┴└──┘└┘ ┴ ┴┴ ┴└──┘└┘ ┴ └┘ ┴┴
st └────────────────────┘ └──────────────────────────────┘
95
96 /-- The `n`th coefficient of a multivariate formal power series.-/
97 def coeff (n : σ →₀ ℕ) : (mv_power_series σ α) →+ α :=
id ┴ └┘ ┴ └─────────────┘ ┴ ┴ └┘ ┴
src └┘ ┴ └─────────────┘ └┘
typ ┴ └┘ ┴ └─────────────┘ ┴ ┴ └┘ ┴
doc └┘ └─────────────┘ └┘
98 { to_fun := λ φ, φ n,
id ┴ ┴ ┴
typ ┴ ┴ ┴
99 map_zero' := rfl,
id └─┘
src └─┘
typ └─┘
100 map_add' := λ _ _, rfl }
id ┴ ┴ └─┘
src └─┘
typ ┴ ┴ └─┘
101
102 variables {α}
103
104 /-- Two multivariate formal power series are equal if all their coefficients are equal.-/
105 @[ext] lemma ext {φ ψ} (h : ∀ (n : σ →₀ ℕ), coeff α n φ = coeff α n ψ) :
id ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src └┘ ┴ └───┘ ┴ └───┘
typ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
doc └─┘ └┘ └───┘ └───┘
106 φ = ψ :=
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
107 funext h
id └────┘ ┴
src └────┘
typ └────┘ ┴
108
109 /-- Two multivariate formal power series are equal
110 if and only if all their coefficients are equal.-/
111 lemma ext_iff {φ ψ : mv_power_series σ α} :
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
doc └─────────────┘
112 φ = ψ ↔ (∀ (n : σ →₀ ℕ), coeff α n φ = coeff α n ψ) :=
id ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src ┴ ┴ └┘ ┴ └───┘ ┴ └───┘
typ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
doc └┘ └───┘ └───┘
113 ⟨λ h n, congr_arg (coeff α n) h, ext⟩
id ┴ ┴ └───────┘ └───┘ ┴ ┴ ┴ └─┘
src └───────┘ └───┘ └─┘
typ ┴ ┴ └───────┘ └───┘ ┴ ┴ ┴ └─┘
doc └───┘ └─┘
114
115 lemma coeff_monomial (m n : σ →₀ ℕ) (a : α) :
id ┴ └┘ ┴ ┴
src └┘ ┴
typ ┴ └┘ ┴ ┴
doc └┘
116 coeff α m (monomial α n a) = if m = n then a else 0 := rfl
id └───┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └───┘ └──────┘ ┴ ┴ └─┘
typ └───┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └───┘ └──────┘
117
118 @[simp] lemma coeff_monomial' (n : σ →₀ ℕ) (a : α) :
id ┴ └┘ ┴ ┴
src └┘ ┴
typ ┴ └┘ ┴ ┴
doc └──┘ └┘
119 coeff α n (monomial α n a) = a := if_pos rfl
id └───┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └────┘ └─┘
src └───┘ └──────┘ ┴ └────┘ └─┘
typ └───┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └────┘ └─┘
doc └───┘ └──────┘
120
121 @[simp] lemma coeff_comp_monomial (n : σ →₀ ℕ) :
id ┴ └┘ ┴
src └┘ ┴
typ ┴ └┘ ┴
doc └──┘ └┘
122 (coeff α n).comp (monomial α n) = add_monoid_hom.id α :=
id └───┘ ┴ ┴ └──┘ └──────┘ ┴ ┴ ┴ └───────────────┘ ┴
src └───┘ └──┘ └──────┘ ┴ └───────────────┘
typ └───┘ ┴ ┴ └──┘ └──────┘ ┴ ┴ ┴ └───────────────┘ ┴
doc └───┘ └──────┘
123 add_monoid_hom.ext $ coeff_monomial' n
id └────────────────┘ └─────────────┘ ┴
src └────────────────┘ └─────────────┘
typ └────────────────┘ └─────────────┘ ┴
124
125 @[simp] lemma coeff_zero (n : σ →₀ ℕ) : coeff α n (0 : mv_power_series σ α) = 0 := rfl
id ┴ └┘ ┴ └───┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └─┘
src └┘ ┴ └───┘ └─────────────┘ ┴ └─┘
typ ┴ └┘ ┴ └───┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └─┘
doc └──┘ └┘ └───┘ └─────────────┘
126
127 end add_monoid
128
129 section semiring
130 variables [semiring α] (n : σ →₀ ℕ) (φ ψ : mv_power_series σ α)
id └──────┘ └┘ ┴ └─────────────┘
src └──────┘ └┘ ┴ └─────────────┘
typ └──────┘ └┘ ┴ └─────────────┘
doc └┘ └─────────────┘
131
132 instance : has_one (mv_power_series σ α) := ⟨monomial α (0 : σ →₀ ℕ) 1⟩
id └─────┘ └─────────────┘ ┴ ┴ └──────┘ ┴ ┴ └┘ ┴
src └─────┘ └─────────────┘ └──────┘ └┘ ┴
typ └─────┘ └─────────────┘ ┴ ┴ └──────┘ ┴ ┴ └┘ ┴
doc └─────────────┘ └──────┘ └┘
133
134 lemma coeff_one :
135 coeff α n (1 : mv_power_series σ α) = if n = 0 then 1 else 0 := rfl
id └───┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └───┘ └─────────────┘ ┴ ┴ └─┘
typ └───┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ └─┘
doc └───┘ └─────────────┘
136
137 @[simp] lemma coeff_zero_one : coeff α (0 : σ →₀ ℕ) 1 = 1 :=
id └───┘ ┴ ┴ └┘ ┴ ┴
src └───┘ └┘ ┴ ┴
typ └───┘ ┴ ┴ └┘ ┴ ┴
doc └──┘ └───┘ └┘
138 coeff_monomial' 0 1
id └─────────────┘
src └─────────────┘
typ └─────────────┘
139
140 instance : has_mul (mv_power_series σ α) :=
id └─────┘ └─────────────┘ ┴ ┴
src └─────┘ └─────────────┘
typ └─────┘ └─────────────┘ ┴ ┴
doc └─────────────┘
141 ⟨λ φ ψ n, (finsupp.antidiagonal n).support.sum (λ p, φ p.1 * ψ p.2)⟩
id ┴ ┴ ┴ └──────────────────┘ ┴ └─────┘ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴┴
src └──────────────────┘ └─────┘ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴ └──────────────────┘ ┴ └─────┘ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴┴
142
143 lemma coeff_mul : coeff α n (φ * ψ) =
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
144 (finsupp.antidiagonal n).support.sum (λ p, coeff α p.1 φ * coeff α p.2 ψ) := rfl
id └──────────────────┘ ┴ └─────┘ └─┘ ┴ └───┘ ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴┴ ┴ └─┘
src └──────────────────┘ └─────┘ └─┘ └───┘ ┴ ┴ └───┘ ┴ └─┘
typ └──────────────────┘ ┴ └─────┘ └─┘ ┴ └───┘ ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴┴ ┴ └─┘
doc └───┘ └───┘
145
146 protected lemma zero_mul : (0 : mv_power_series σ α) * φ = 0 :=
id └─────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
147 ext $ λ n, by simp [coeff_mul]
id └─┘ ┴ └───────┘
src └─┘ └────┘└───────┘└─
typ └─┘ ┴ └────┘└───────┘└─
doc └─┘ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └─────────────────
148
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
149 protected lemma mul_zero : φ * 0 = 0 :=
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
150 ext $ λ n, by simp [coeff_mul]
id └─┘ ┴ └───────┘
src └─┘ └────┘└───────┘└─
typ └─┘ ┴ └────┘└───────┘└─
doc └─┘ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └─────────────────
151
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
152 protected lemma one_mul : (1 : mv_power_series σ α) * φ = φ :=
id └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
153 ext $ λ n,
id └─┘ ┴
src └─┘
typ └─┘ ┴
doc └─┘
154 begin
st └─────
155 rw [coeff_mul, finset.sum_eq_single ((0 : σ →₀ ℕ), n)];
id └───────┘ └──────────────────┘ ┴ ┴ └┘ ┴
src └──┘└───────┘└┘└──────────────────┘┴┴ └──┘ ┴└┘┴ └─┘ └┘
typ └──┘└───────┘└┘└──────────────────┘┴┴ └──┘┴┴└┘┴ └─┘┴└┘
doc └──┘ └┘ ┴ └──┘ ┴└┘┴ └─┘ └┘
txt └──┘ └┘ ┴ └──┘ ┴ ┴ └─┘ └┘
par └──┘ └┘ ┴ └──┘ ┴ ┴ └─┘ └┘
pid └┘ └┘ ┴ └──┘ ┴ ┴ └─┘ └┘
st ──────────────┘└──────────────────────────────────────┘┴└─
156 simp [mem_antidiagonal_support, coeff_one],
id └──────────────────────┘ └───────┘
src └────┘└──────────────────────┘└┘└───────┘┴
typ └────┘└──────────────────────┘└┘└───────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ───────────────────────────────────────────┘└─
157 show ∀ (i j : σ →₀ ℕ), i + j = n → (i = 0 → j ≠ n) →
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └──────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴ └─┘ ┴ ┴┴┴ └┘ └
typ └───┘ └──────┘┴┴ ┴ ┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴┴└─┘┴┴ ┴┴┴┴└┘ └
doc └───┘ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ └
txt └───┘ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ └
par └───┘ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ └
pid └───┘ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ └
st ───────────────────────────────────────────────────────
158 (if (i = 0) then 1 else 0) * (coeff α j) φ = 0,
id ┴ └───┘ ┴ ┴
src ───┘ ┴ ┴ └─────────────────┘┴┴ └───┘┴ ┴ └┘ ┴ └┘
typ ───┘ ┴ ┴ └─────────────────┘┴┴ └───┘┴┴┴ └┘┴┴ └┘
doc ───┘ ┴ ┴ └─────────────────┘ ┴ └───┘┴ ┴ └┘ ┴ └┘
txt ───┘ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ └┘ ┴ └┘
par ───┘ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ └┘ ┴ └┘
pid ───┘ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ └┘ ┴ ┴┴
st ─────────────────────────────────────────────────┘└─
159 intros i j hij h,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ─────────────────┘└─
160 rw [if_neg, zero_mul],
id └────┘ └──────┘
src └──┘└────┘└┘└──────┘┴
typ └──┘└────┘└┘└──────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────┘└────────┘└──
161 contrapose! h,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid ┴└┘
st ──────────────┘└─
162 simpa [h] using hij,
id ┴ └─┘
src └─────┘ └──────┘
typ └─────┘┴└──────┘└─┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st ────────────────────┘└─
163 end
st ──┘
164
165 protected lemma mul_one : φ * 1 = φ :=
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
166 ext $ λ n,
id └─┘ ┴
src └─┘
typ └─┘ ┴
doc └─┘
167 begin
st └─────
168 rw [coeff_mul, finset.sum_eq_single (n, (0 : σ →₀ ℕ))],
id └───────┘ └──────────────────┘ ┴┴ ┴ └┘
src └──┘└───────┘└┘└──────────────────┘┴┴ └┘ └──┘ ┴└┘┴ └─┘
typ └──┘└───────┘└┘└──────────────────┘┴┴┴└┘ └──┘┴┴└┘┴ └─┘
doc └──┘ └┘ ┴ └┘ └──┘ ┴└┘┴ └─┘
txt └──┘ └┘ ┴ └┘ └──┘ ┴ ┴ └─┘
par └──┘ └┘ ┴ └┘ └──┘ ┴ ┴ └─┘
pid └┘ └┘ ┴ └┘ └──┘ ┴ ┴ └─┘
st ──────────────┘└──────────────────────────────────────┘└──
169 rotate,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ───────┘└─
170 { rintros ⟨i, j⟩ hij h,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └───────────┘
st ───┘└──────────────────┘└─
171 rw [coeff_one, if_neg, mul_zero],
id └───────┘ └────┘ └──────┘
src └──┘└───────┘└┘└────┘└┘└──────┘┴
typ └──┘└───────┘└┘└────┘└┘└──────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ────────────────┘└──────┘└────────┘└──
172 rw mem_antidiagonal_support at hij,
id └──────────────────────┘
src └─┘└──────────────────────┘└─────┘
typ └─┘└──────────────────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ─────────────────────────────────────┘└─
173 contrapose! h,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid ┴└┘
st ────────────────┘└─
174 simpa [h] using hij },
id ┴ └─┘
src └─────┘ └──────┘ ┴
typ └─────┘┴└──────┘└─┘┴
doc └─────┘ └──────┘ ┴
txt └─────┘ └──────┘ ┴
par └─────┘ └──────┘ ┴
pid ┴┴ ┴┴└────┘ ┴
st ───────────────────────┘└┘└
175 all_goals { simp [mem_antidiagonal_support, coeff_one] }
id └──────────────────────┘ └───────┘
src └──────────┘└────┘└──────────────────────┘└┘└───────┘└┘└┘
typ └──────────┘└────┘└──────────────────────┘└┘└───────┘└┘└┘
doc └──────────┘└────┘ └┘ └┘└┘
txt └──────────┘└────┘ └┘ └┘└┘
par └──────────┘└────┘ └┘ └┘└┘
pid └───────┘ └┘ └─┘┴
st ────────────┘└──────────────────────────────────────────┘┴┴
176 end
st └─┘
177
178 protected lemma mul_add (φ₁ φ₂ φ₃ : mv_power_series σ α) :
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
doc └─────────────┘
179 φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃ :=
id └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘
src ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘
180 ext $ λ n, by simp only [coeff_mul, mul_add, finset.sum_add_distrib, add_monoid_hom.map_add]
id └─┘ ┴ └───────┘ └─────┘ └────────────────────┘ └────────────────────┘
src └─┘ └─────────┘└───────┘└┘└─────┘└┘└────────────────────┘└┘└────────────────────┘└─
typ └─┘ ┴ └─────────┘└───────┘└┘└─────┘└┘└────────────────────┘└┘└────────────────────┘└─
doc └─┘ └─────────┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ ┴└
st └───────────────────────────────────────────────────────────────────────────────
181
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
182 protected lemma add_mul (φ₁ φ₂ φ₃ : mv_power_series σ α) :
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
doc └─────────────┘
183 (φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃ :=
id └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘
src ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘
184 ext $ λ n, by simp only [coeff_mul, add_mul, finset.sum_add_distrib, add_monoid_hom.map_add]
id └─┘ ┴ └───────┘ └─────┘ └────────────────────┘ └────────────────────┘
src └─┘ └─────────┘└───────┘└┘└─────┘└┘└────────────────────┘└┘└────────────────────┘└─
typ └─┘ ┴ └─────────┘└───────┘└┘└─────┘└┘└────────────────────┘└┘└────────────────────┘└─
doc └─┘ └─────────┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ ┴└
st └───────────────────────────────────────────────────────────────────────────────
185
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
186 protected lemma mul_assoc (φ₁ φ₂ φ₃ : mv_power_series σ α) :
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
doc └─────────────┘
187 (φ₁ * φ₂) * φ₃ = φ₁ * (φ₂ * φ₃) :=
id └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘
src ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘
188 ext $ λ n,
id └─┘ ┴
src └─┘
typ └─┘ ┴
doc └─┘
189 begin
st └─────
190 simp only [coeff_mul],
id └───────┘
src └─────────┘└───────┘┴
typ └─────────┘└───────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────┘└─
191 have := @finset.sum_sigma ((σ →₀ ℕ) × (σ →₀ ℕ)) α _ _ (antidiagonal n).support
id └──────────────┘ └┘ ┴ ┴ ┴
src └──────┘ └──────────────┘┴ ┴└┘┴ └┘┴┴ ┴ ┴ └─┘ └───┘ ┴ └─────────
typ └──────┘ └──────────────┘┴ ┴└┘┴ └┘┴┴ ┴┴ ┴ └─┘ └───┘ ┴┴└─────────
doc └──────┘ ┴ ┴└┘┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └─────────
txt └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └─────────
par └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └─────────
pid └───┘└─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └─────────
st ─────────────────────────────────────────────────────────────────────────────────
192 (λ p, (antidiagonal (p.1)).support) (λ x, coeff α x.2.1 φ₁ * coeff α x.2.2 φ₂ * coeff α x.1.2 φ₃),
id └──────────┘ └┘ ┴ └┘ └───┘ ┴ └┘
src ───┘ └──┘ └──────────┘┴ └────────────┘ └──┘ ┴ ┴ └───┘ ┴┴┴ ┴ ┴ └───┘ ┴ ┴└───┘┴ ┴ └───┘ ┴
typ ───┘ └──┘ └──────────┘┴ └────────────┘ └──┘ ┴ ┴ └───┘└┘┴┴┴ ┴ ┴ └───┘└┘┴ ┴└───┘┴┴┴ └───┘└┘┴
doc ───┘ └──┘ ┴ └────────────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴└───┘┴ ┴ └───┘ ┴
txt ───┘ └──┘ ┴ └────────────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴
par ───┘ └──┘ ┴ └────────────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴
pid ───┘ └──┘ ┴ └────────────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
193 convert this.symm using 1; clear this,
id └───────┘
src └──────┘└───────┘└──────┘ └────────┘
typ └──────┘└───────┘└──────┘ └────────┘
doc └──────┘ └──────┘ └────────┘
txt └──────┘ └──────┘ └────────┘
par └──────┘ └──────┘ └────────┘
pid ┴ └─────┘┴ └───┘
st ──────────────────────────────────────┘└─
194 { apply finset.sum_congr rfl,
id └──────────────┘ └─┘
src └────┘└──────────────┘┴└─┘
typ └────┘└──────────────┘┴└─┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└────────────────────────┘└─
195 intros p hp, exact finset.sum_mul },
id └────────────┘
src └─────────┘ └────┘└────────────┘┴
typ └─────────┘ └────┘└────────────┘┴
doc └─────────┘ └────┘ ┴
txt └─────────┘ └────┘ ┴
par └─────────┘ └────┘ ┴
pid └───┘ ┴ ┴
st ──────────────┘└─────────────────────┘└┘└
196 have := @finset.sum_sigma ((σ →₀ ℕ) × (σ →₀ ℕ)) α _ _ (antidiagonal n).support
id └──────────────┘ ┴ ┴
src └──────┘ └──────────────┘┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └─────────
typ └──────┘ └──────────────┘┴ ┴ ┴ └┘ ┴ ┴┴ ┴ └─┘ └───┘ ┴┴└─────────
doc └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └─────────
txt └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └─────────
par └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └─────────
pid └───┘└─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴ └─────────
st ─────────────────────────────────────────────────────────────────────────────────
197 (λ p, (antidiagonal (p.2)).support) (λ x, coeff α x.1.1 φ₁ * (coeff α x.2.1 φ₂ * coeff α x.2.2 φ₃)),
id └──────────┘ └┘ └┘ └───┘ ┴ └┘
src ───┘ └──┘ └──────────┘┴ └────────────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴└───┘┴ ┴ └───┘ └┘
typ ───┘ └──┘ └──────────┘┴ └────────────┘ └──┘ ┴ ┴ └───┘└┘┴ ┴ ┴ ┴ └───┘└┘┴ ┴└───┘┴┴┴ └───┘└┘└┘
doc ───┘ └──┘ ┴ └────────────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴└───┘┴ ┴ └───┘ └┘
txt ───┘ └──┘ ┴ └────────────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ └┘
par ───┘ └──┘ ┴ └────────────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ └┘
pid ───┘ └──┘ ┴ └────────────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ └┘
st ──────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
198 convert this.symm using 1; clear this,
id └───────┘
src └──────┘└───────┘└──────┘ └────────┘
typ └──────┘└───────┘└──────┘ └────────┘
doc └──────┘ └──────┘ └────────┘
txt └──────┘ └──────┘ └────────┘
par └──────┘ └──────┘ └────────┘
pid ┴ └─────┘┴ └───┘
st ──────────────────────────────────────┘└─
199 { apply finset.sum_congr rfl, intros p hp, rw finset.mul_sum },
id └──────────────┘ └─┘ └────────────┘
src └────┘└──────────────┘┴└─┘ └─────────┘ └─┘└────────────┘┴
typ └────┘└──────────────┘┴└─┘ └─────────┘ └─┘└────────────┘┴
doc └────┘ ┴ └─────────┘ └─┘ ┴
txt └────┘ ┴ └─────────┘ └─┘ ┴
par └────┘ ┴ └─────────┘ └─┘ ┴
pid ┴ ┴ └───┘ ┴ ┴
st ───┘└────────────────────────┘└───────────┘└──────────────────┘└┘└
200 apply finset.sum_bij,
id └────────────┘
src └────┘└────────────┘
typ └────┘└────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
201 swap 5,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴┴
st ───────┘└─
202 { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, exact ⟨(k, l+j), (l, j)⟩ },
id ┴┴ ┴ ┴ ┴
src └──────────────────────┘ └────┘ ┴ └┘ ┴ └─┘ └┘ └─┘
typ └──────────────────────┘ └────┘ ┴┴└┘ ┴ └─┘ ┴└┘┴└─┘
doc └──────────────────────┘ └────┘ └┘ └─┘ └┘ └─┘
txt └──────────────────────┘ └────┘ └┘ └─┘ └┘ └─┘
par └──────────────────────┘ └────┘ └┘ └─┘ └┘ └─┘
pid └───────────────┘ ┴ └┘ └─┘ └┘ └┘┴
st ───┘└──────────────────────┘└─────────────────────────┘└┘└
203 { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H,
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
txt └──────────────────────┘
par └──────────────────────┘
pid └───────────────┘
st ───┘└──────────────────────┘└─
204 simp only [finset.mem_sigma, mem_antidiagonal_support] at H ⊢, finish },
id └──────────────┘ └──────────────────────┘
src └─────────┘└──────────────┘└┘└──────────────────────┘└──────┘ └─────┘
typ └─────────┘└──────────────┘└┘└──────────────────────┘└──────┘ └─────┘
doc └─────────┘ └┘ └──────┘ └─────┘
txt └─────────┘ └┘ └──────┘ └─────┘
par └─────────┘ └┘ └──────┘ └─────┘
pid ┴└──┘└┘ └┘ ┴┴└────┘ ┴
st ────────────────────────────────────────────────────────────────┘└───────┘└┘└
205 { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, rw mul_assoc },
id └───────┘
src └──────────────────────┘ └─┘└───────┘┴
typ └──────────────────────┘ └─┘└───────┘┴
doc └──────────────────────┘ └─┘ ┴
txt └──────────────────────┘ └─┘ ┴
par └──────────────────────┘ └─┘ ┴
pid └───────────────┘ ┴ ┴
st ───┘└──────────────────────┘└─────────────┘└┘└
206 { rintros ⟨⟨a,b⟩, ⟨c,d⟩⟩ ⟨⟨i,j⟩, ⟨k,l⟩⟩ H₁ H₂,
src └─────────────────────────────────────────┘
typ └─────────────────────────────────────────┘
doc └─────────────────────────────────────────┘
txt └─────────────────────────────────────────┘
par └─────────────────────────────────────────┘
pid └──────────────────────────────────┘
st ───┘└─────────────────────────────────────────┘└─
207 simp only [finset.mem_sigma, mem_antidiagonal_support,
id └──────────────┘ └──────────────────────┘
src └─────────┘└──────────────┘└┘└──────────────────────┘└─
typ └─────────┘└──────────────┘└┘└──────────────────────┘└─
doc └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ └─
st ───────────────────────────────────────────────────────────
208 and_imp, prod.mk.inj_iff, add_comm, heq_iff_eq] at H₁ H₂ ⊢,
id └─────┘ └─────────────┘ └──────┘ └────────┘
src ─────┘└─────┘└┘└─────────────┘└┘└──────┘└┘└────────┘└──────────┘
typ ─────┘└─────┘└┘└─────────────┘└┘└──────┘└┘└────────┘└──────────┘
doc ─────┘ └┘ └┘ └┘ └──────────┘
txt ─────┘ └┘ └┘ └┘ └──────────┘
par ─────┘ └┘ └┘ └┘ └──────────┘
pid ─────┘ └┘ └┘ └┘ ┴┴└────────┘
st ───────────────────────────────────────────────────────────────┘└─
209 finish },
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴
st ──────────┘└┘└
210 { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, refine ⟨⟨(i+k, l), (i, k)⟩, _, _⟩;
id ┴ ┴ ┴
src └──────────────────────┘ └─────┘ └┘ └─┘ └┘ └───────┘
typ └──────────────────────┘ └─────┘ └┘┴└─┘ ┴└┘┴└───────┘
doc └──────────────────────┘ └─────┘ └┘ └─┘ └┘ └───────┘
txt └──────────────────────┘ └─────┘ └┘ └─┘ └┘ └───────┘
par └──────────────────────┘ └─────┘ └┘ └─┘ └┘ └───────┘
pid └───────────────┘ ┴ └┘ └─┘ └┘ └───────┘
st ───────────────────────────┘└────────────────────────────────────
211 { simp only [finset.mem_sigma, mem_antidiagonal_support] at H ⊢, finish } }
id └──────────────┘ └──────────────────────┘
src └─────────┘└──────────────┘└┘└──────────────────────┘└──────┘ └─────┘
typ └─────────┘└──────────────┘└┘└──────────────────────┘└──────┘ └─────┘
doc └─────────┘ └┘ └──────┘ └─────┘
txt └─────────┘ └┘ └──────┘ └─────┘
par └─────────┘ └┘ └──────┘ └─────┘
pid ┴└──┘└┘ └┘ ┴┴└────┘ ┴
st ───┘└─────────────────────────────────────────────────────────────┘└───────┘└───
212 end
st ──┘
213
214 instance : semiring (mv_power_series σ α) :=
id └──────┘ └─────────────┘ ┴ ┴
src └──────┘ └─────────────┘
typ └──────┘ └─────────────┘ ┴ ┴
doc └─────────────┘
215 { mul_one := mv_power_series.mul_one,
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
216 one_mul := mv_power_series.one_mul,
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
217 mul_assoc := mv_power_series.mul_assoc,
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
218 mul_zero := mv_power_series.mul_zero,
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
219 zero_mul := mv_power_series.zero_mul,
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
220 left_distrib := mv_power_series.mul_add,
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
221 right_distrib := mv_power_series.add_mul,
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
222 .. mv_power_series.has_one,
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
223 .. mv_power_series.has_mul,
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
224 .. mv_power_series.add_comm_monoid }
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
225
226 end semiring
227
228 instance [comm_semiring α] : comm_semiring (mv_power_series σ α) :=
id └───────────┘ ┴ └───────────┘ └─────────────┘ ┴ ┴
src └───────────┘ └───────────┘ └─────────────┘
typ └───────────┘ ┴ └───────────┘ └─────────────┘ ┴ ┴
doc └─────────────┘
229 { mul_comm := λ φ ψ, ext $ λ n, finset.sum_bij (λ p hp, p.swap)
id ┴ ┴ └─┘ ┴ └────────────┘ ┴ └┘ ┴└───┘
src └─┘ └────────────┘ └───┘
typ ┴ ┴ └─┘ ┴ └────────────┘ ┴ └┘ ┴└───┘
doc └─┘ └───┘
230 (λ p hp, swap_mem_antidiagonal_support hp)
id ┴ └┘ └───────────────────────────┘ └┘
src └───────────────────────────┘
typ ┴ └┘ └───────────────────────────┘ └┘
231 (λ p hp, mul_comm _ _)
id ┴ └┘ └──────┘
src └──────┘
typ ┴ └┘ └──────┘
232 (λ p q hp hq H, by simpa using congr_arg prod.swap H)
id ┴ ┴ └┘ └┘ ┴ └───────┘ └───────┘ ┴
src └──────────┘└───────┘┴└───────┘┴
typ ┴ ┴ └┘ └┘ ┴ └──────────┘└───────┘┴└───────┘┴┴
doc └──────────┘ ┴└───────┘┴
txt └──────────┘ ┴ ┴
par └──────────┘ ┴ ┴
pid ┴└────┘ ┴ ┴
st └────────────────────────────────┘
233 (λ p hp, ⟨p.swap, swap_mem_antidiagonal_support hp, p.swap_swap.symm⟩),
id ┴ └┘ ┴└───┘ └───────────────────────────┘ └┘ ┴└────────┘└───┘
src └───┘ └───────────────────────────┘ └────────┘└───┘
typ ┴ └┘ ┴└───┘ └───────────────────────────┘ └┘ ┴└────────┘└───┘
doc └───┘
234 .. mv_power_series.semiring }
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
235
236 instance [ring α] : ring (mv_power_series σ α) :=
id └──┘ ┴ └──┘ └─────────────┘ ┴ ┴
src └──┘ └──┘ └─────────────┘
typ └──┘ ┴ └──┘ └─────────────┘ ┴ ┴
doc └─────────────┘
237 { .. mv_power_series.semiring,
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
238 .. mv_power_series.add_comm_group }
id └────────────────────────────┘
src └────────────────────────────┘
typ └────────────────────────────┘
239
240 instance [comm_ring α] : comm_ring (mv_power_series σ α) :=
id └───────┘ ┴ └───────┘ └─────────────┘ ┴ ┴
src └───────┘ └───────┘ └─────────────┘
typ └───────┘ ┴ └───────┘ └─────────────┘ ┴ ┴
doc └─────────────┘
241 { .. mv_power_series.comm_semiring,
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
242 .. mv_power_series.add_comm_group }
id └────────────────────────────┘
src └────────────────────────────┘
typ └────────────────────────────┘
243
244 section semiring
245 variables [semiring α]
id └──────┘
src └──────┘
typ └──────┘
246
247 lemma monomial_mul_monomial (m n : σ →₀ ℕ) (a b : α) :
id ┴ └┘ ┴ ┴
src └┘ ┴
typ ┴ └┘ ┴ ┴
doc └┘
248 monomial α m a * monomial α n b = monomial α (m + n) (a * b) :=
id └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘ └──────┘
249 begin
st └─────
250 ext k, rw [coeff_mul, coeff_monomial], split_ifs with h,
id └───────┘ └────────────┘
src └───┘ └──┘└───────┘└┘└────────────┘┴ └──────────────┘
typ └───┘ └──┘└───────┘└┘└────────────┘┴ └──────────────┘
doc └───┘ └──┘ └┘ ┴ └──────────────┘
txt └───┘ └──┘ └┘ ┴ └──────────────┘
par └───┘ └──┘ └┘ ┴ └──────────────┘
pid └┘ └┘ └┘ ┴ ┴└────┘
st ──────┘└─────────────┘└──────────────┘└─────────────────┘└─
251 { rw [h, finset.sum_eq_single (m,n)],
id ┴ └──────────────────┘ ┴┴ ┴
src └──┘ └┘└──────────────────┘┴┴ ┴ └┘
typ └──┘┴└┘└──────────────────┘┴┴┴┴┴└┘
doc └──┘ └┘ ┴ ┴ └┘
txt └──┘ └┘ ┴ ┴ └┘
par └──┘ └┘ ┴ ┴ └┘
pid └┘ └┘ ┴ ┴ └┘
st ───┘└───┘└──────────────────────────┘└──
252 { rw [coeff_monomial', coeff_monomial'] },
id └─────────────┘ └─────────────┘
src └──┘└─────────────┘└┘└─────────────┘└┘
typ └──┘└─────────────┘└┘└─────────────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ─────┘└─────────────────┘└───────────────┘┴┴└┘└
253 { rintros ⟨i,j⟩ hij hne,
src └───────────────────┘
typ └───────────────────┘
doc └───────────────────┘
txt └───────────────────┘
par └───────────────────┘
pid └────────────┘
st ─────┘└───────────────────┘└─
254 rw [ne.def, prod.mk.inj_iff, not_and] at hne,
id └────┘ └─────────────┘ └─────┘
src └──┘└────┘└┘└─────────────┘└┘└─────┘└──────┘
typ └──┘└────┘└┘└─────────────┘└┘└─────┘└──────┘
doc └──┘ └┘ └┘ └──────┘
txt └──┘ └┘ └┘ └──────┘
par └──┘ └┘ └┘ └──────┘
pid └┘ └┘ └┘ ┴└─────┘
st ───────────────┘└───────────────┘└───────┘┴└─────┘└─
255 by_cases H : i = m,
id ┴ ┴ ┴
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ───────────────────────┘└─
256 { rw [coeff_monomial j n b, if_neg (hne H), mul_zero] },
id └────────────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ └──────┘
src └──┘└────────────┘┴ ┴ ┴ └┘└────┘┴ ┴ └─┘└──────┘└┘
typ └──┘└────────────┘┴┴┴┴┴┴└┘└────┘┴ └─┘┴┴└─┘└──────┘└┘
doc └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ └┘
txt └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ └┘
par └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ └┘
pid └┘ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴┴
st ───────┘└──────────────────────┘└──────────────┘└────────┘┴┴└┘└
257 { rw [coeff_monomial, if_neg H, zero_mul] } },
id └────────────┘ └────┘ ┴ └──────┘
src └──┘└────────────┘└┘└────┘┴ └┘└──────┘└┘
typ └──┘└────────────┘└┘└────┘┴┴└┘└──────┘└┘
doc └──┘ └┘ ┴ └┘ └┘
txt └──┘ └┘ ┴ └┘ └┘
par └──┘ └┘ ┴ └┘ └┘
pid └┘ └┘ ┴ └┘ ┴┴
st ─────────────────────────┘└────────┘└────────┘┴┴└──┘└
258 { intro H, rw finsupp.mem_antidiagonal_support at H,
id └──────────────────────────────┘
src └─────┘ └─┘└──────────────────────────────┘└───┘
typ └─────┘ └─┘└──────────────────────────────┘└───┘
doc └─────┘ └─┘ └───┘
txt └─────┘ └─┘ └───┘
par └─────┘ └─┘ └───┘
pid └┘ ┴ └───┘
st ────────────┘└────────────────────────────────────────┘└─
259 exfalso, exact H rfl } },
id ┴ └─┘
src └─────┘ └────┘ ┴└─┘┴
typ └─────┘ └────┘┴┴└─┘┴
doc └─────┘ └────┘ ┴ ┴
txt └─────┘ └────┘ ┴ ┴
par └─────┘ └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────┘└────────────┘└──┘└
260 { rw [finset.sum_eq_zero], rintros ⟨i,j⟩ hij,
id └────────────────┘
src └──┘└────────────────┘┴ └───────────────┘
typ └──┘└────────────────┘┴ └───────────────┘
doc └──┘ ┴ └───────────────┘
txt └──┘ ┴ └───────────────┘
par └──┘ ┴ └───────────────┘
pid └┘ ┴ └────────┘
st ─────────────────────────┘└──────────────────┘└─
261 rw finsupp.mem_antidiagonal_support at hij,
id └──────────────────────────────┘
src └─┘└──────────────────────────────┘└─────┘
typ └─┘└──────────────────────────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ─────────────────────────────────────────────┘└─
262 by_cases H : i = m,
id ┴ ┴
src └───────┘ └─┘ ┴ ┴
typ └───────┘ └─┘┴┴ ┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ─────────────────────┘└─
263 { subst i, have : j ≠ n, { rintro rfl, exact h hij.symm },
id ┴ ┴ ┴ ┴ ┴ └──────┘
src └────┘ └─────┘ ┴┴┴ └────────┘ └────┘ ┴└──────┘┴
typ └────┘┴ └─────┘┴┴┴┴┴ └────────┘ └────┘┴┴└──────┘┴
doc └────┘ └─────┘ ┴ ┴ └────────┘ └────┘ ┴ ┴
txt └────┘ └─────┘ ┴ ┴ └────────┘ └────┘ ┴ ┴
par └────┘ └─────┘ ┴ ┴ └────────┘ └────┘ ┴ ┴
pid ┴ └───┘└┘ ┴ ┴ └──┘ ┴ ┴ ┴
st ─────┘└─────┘└────────────┘└──┘└────────┘└─────────────────┘└┘└
264 { rw [coeff_monomial j n b, if_neg this, mul_zero] } },
id └────────────┘ ┴ ┴ ┴ └────┘ └──┘ └──────┘
src └──┘└────────────┘┴ ┴ ┴ └┘└────┘┴ └┘└──────┘└┘
typ └──┘└────────────┘┴┴┴┴┴┴└┘└────┘┴└──┘└┘└──────┘└┘
doc └──┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘
txt └──┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘
par └──┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘
pid └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴┴
st ───────────────────────────────┘└───────────┘└────────┘┴┴└──┘└
265 { rw [coeff_monomial, if_neg H, zero_mul] } }
id └────────────┘ └────┘ ┴ └──────┘
src └──┘└────────────┘└┘└────┘┴ └┘└──────┘└┘
typ └──┘└────────────┘└┘└────┘┴┴└┘└──────┘└┘
doc └──┘ └┘ ┴ └┘ └┘
txt └──┘ └┘ ┴ └┘ └┘
par └──┘ └┘ ┴ └┘ └┘
pid └┘ └┘ ┴ └┘ ┴┴
st ───────────────────────┘└────────┘└────────┘┴┴└───
266 end
st ──┘
267
268 variables (σ) (α)
269
270 /-- The constant multivariate formal power series.-/
271 def C : α →+* mv_power_series σ α :=
id ┴ └─┘ └─────────────┘ ┴ ┴
src └─┘ └─────────────┘
typ ┴ └─┘ └─────────────┘ ┴ ┴
doc └─┘ └─────────────┘
272 { map_one' := rfl,
id └─┘
src └─┘
typ └─┘
273 map_mul' := λ a b, (monomial_mul_monomial 0 0 a b).symm,
id ┴ ┴ └───────────────────┘ ┴ ┴ └──┘
src └───────────────────┘ └──┘
typ ┴ ┴ └───────────────────┘ ┴ ┴ └──┘
274 .. monomial α (0 : σ →₀ ℕ) }
id └──────┘ ┴ ┴ └┘ ┴
src └──────┘ └┘ ┴
typ └──────┘ ┴ ┴ └┘ ┴
doc └──────┘ └┘
275
276 variables {σ} {α}
277
278 @[simp] lemma monomial_zero_eq_C : monomial α (0 : σ →₀ ℕ) = C σ α := rfl
id └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └──────┘ └┘ ┴ ┴ ┴ └─┘
typ └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └──────┘ └┘ ┴
279
280 @[simp] lemma monomial_zero_eq_C_apply (a : α) : monomial α (0 : σ →₀ ℕ) a = C σ α a := rfl
id ┴ └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └──────┘ └┘ ┴ ┴ ┴ └─┘
typ ┴ └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └──────┘ └┘ ┴
281
282 lemma coeff_C (n : σ →₀ ℕ) (a : α) :
id ┴ └┘ ┴ ┴
src └┘ ┴
typ ┴ └┘ ┴ ┴
doc └┘
283 coeff α n (C σ α a) = if n = 0 then a else 0 := rfl
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └───┘ ┴ ┴ ┴ └─┘
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └───┘ ┴
284
285 @[simp] lemma coeff_zero_C (a : α) : coeff α (0 : σ →₀ℕ) (C σ α a) = a :=
id ┴ └───┘ ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └┘┴ ┴ ┴
typ ┴ └───┘ ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └───┘ └┘ ┴
286 coeff_monomial' 0 a
id └─────────────┘ ┴
src └─────────────┘
typ └─────────────┘ ┴
287
288 /-- The variables of the multivariate formal power series ring.-/
289 def X (s : σ) : mv_power_series σ α := monomial α (single s 1) 1
id ┴ └─────────────┘ ┴ ┴ └──────┘ ┴ └────┘ ┴
src └─────────────┘ └──────┘ └────┘
typ ┴ └─────────────┘ ┴ ┴ └──────┘ ┴ └────┘ ┴
doc └─────────────┘ └──────┘ └────┘
290
291 lemma coeff_X (n : σ →₀ ℕ) (s : σ) :
id ┴ └┘ ┴ ┴
src └┘ ┴
typ ┴ └┘ ┴ ┴
doc └┘
292 coeff α n (X s : mv_power_series σ α) = if n = (single s 1) then 1 else 0 := rfl
id └───┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └─┘
src └───┘ ┴ └─────────────┘ ┴ ┴ └────┘ └─┘
typ └───┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └─┘
doc └───┘ ┴ └─────────────┘ └────┘
293
294 lemma coeff_index_single_X (s t : σ) :
id ┴
typ ┴
295 coeff α (single t 1) (X s : mv_power_series σ α) = if t = s then 1 else 0 :=
id └───┘ ┴ └────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └────┘ ┴ └─────────────┘ ┴ ┴
typ └───┘ ┴ └────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └────┘ ┴ └─────────────┘
296 by { simp only [coeff_X, single_right_inj one_ne_zero], split_ifs; refl }
id └─────┘ └──────────────┘ └─────────┘
src └─────────┘└─────┘└┘└──────────────┘┴└─────────┘┴ └───────┘ └───┘
typ └─────────┘└─────┘└┘└──────────────┘┴└─────────┘┴ └───────┘ └───┘
doc └─────────┘ └┘ ┴ ┴ └───────┘ └───┘
txt └─────────┘ └┘ ┴ ┴ └───────┘ └───┘
par └─────────┘ └┘ ┴ ┴ └───────┘ └───┘
pid ┴└──┘└┘ └┘ ┴ ┴ ┴
st └──────────────────────────────────────────────────┘└────────────────┘└┘
297
298 @[simp] lemma coeff_index_single_self_X (s : σ) :
id ┴
typ ┴
doc └──┘
299 coeff α (single s 1) (X s : mv_power_series σ α) = 1 :=
id └───┘ ┴ └────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └───┘ └────┘ ┴ └─────────────┘ ┴
typ └───┘ ┴ └────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └───┘ └────┘ ┴ └─────────────┘
300 if_pos rfl
id └────┘ └─┘
src └────┘ └─┘
typ └────┘ └─┘
301
302 @[simp] lemma coeff_zero_X (s : σ) : coeff α (0 : σ →₀ ℕ) (X s : mv_power_series σ α) = 0 :=
id ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └───┘ └┘ ┴ ┴ └─────────────┘ ┴
typ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └──┘ └───┘ └┘ ┴ └─────────────┘
303 by { rw [coeff_X, if_neg], intro h, exact one_ne_zero (single_eq_zero.mp h.symm) }
id └─────┘ └────┘ └─────────┘ └───────────────┘ └────┘
src └──┘└─────┘└┘└────┘┴ └─────┘ └────┘└─────────┘┴ └───────────────┘┴└────┘└┘
typ └──┘└─────┘└┘└────┘┴ └─────┘ └────┘└─────────┘┴ └───────────────┘┴└────┘└┘
doc └──┘ └┘ ┴ └─────┘ └────┘ ┴ ┴ └┘
txt └──┘ └┘ ┴ └─────┘ └────┘ ┴ ┴ └┘
par └──┘ └┘ ┴ └─────┘ └────┘ ┴ ┴ └┘
pid └┘ └┘ ┴ └┘ ┴ ┴ ┴ ┴┴
st └────────────┘└──────┘└────────┘└─────────────────────────────────────────────┘└┘
304
305 lemma X_def (s : σ) : X s = monomial α (single s 1) 1 := rfl
id ┴ ┴ ┴ ┴ └──────┘ ┴ └────┘ ┴ └─┘
src ┴ ┴ └──────┘ └────┘ └─┘
typ ┴ ┴ ┴ ┴ └──────┘ ┴ └────┘ ┴ └─┘
doc ┴ └──────┘ └────┘
306
307 lemma X_pow_eq (s : σ) (n : ℕ) :
id ┴ ┴
src ┴
typ ┴ ┴
308 (X s : mv_power_series σ α)^n = monomial α (single s n) 1 :=
id ┴ ┴ └─────────────┘ ┴ ┴ ┴┴ ┴ └──────┘ ┴ └────┘ ┴ ┴
src ┴ └─────────────┘ ┴ ┴ └──────┘ └────┘
typ ┴ ┴ └─────────────┘ ┴ ┴ ┴┴ ┴ └──────┘ ┴ └────┘ ┴ ┴
doc ┴ └─────────────┘ └──────┘ └────┘
309 begin
st └─────
310 induction n with n ih,
id ┴
src └────────┘ └────────┘
typ └────────┘┴└────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
pid ┴ ┴└───────┘
st ──────────────────────┘└─
311 { rw [pow_zero, finsupp.single_zero], refl },
id └──────┘ └─────────────────┘
src └──┘└──────┘└┘└─────────────────┘┴ └───┘
typ └──┘└──────┘└┘└─────────────────┘┴ └───┘
doc └──┘ └┘ ┴ └───┘
txt └──┘ └┘ ┴ └───┘
par └──┘ └┘ ┴ └───┘
pid └┘ └┘ ┴ ┴
st ───┘└──────────┘└───────────────────┘┴└─────┘└┘└
312 { rw [pow_succ', ih, nat.succ_eq_add_one, finsupp.single_add, X, monomial_mul_monomial, one_mul] }
id └───────┘ └┘ └─────────────────┘ └────────────────┘ ┴ └───────────────────┘ └─────┘
src └──┘└───────┘└┘ └┘└─────────────────┘└┘└────────────────┘└┘┴└┘└───────────────────┘└┘└─────┘└┘
typ └──┘└───────┘└┘└┘└┘└─────────────────┘└┘└────────────────┘└┘┴└┘└───────────────────┘└┘└─────┘└┘
doc └──┘ └┘ └┘ └┘ └┘┴└┘ └┘ └┘
txt └──┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
pid └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴┴
st ────────────────┘└──┘└───────────────────┘└──────────────────┘└─┘└─────────────────────┘└───────┘┴┴└─
313 end
st ──┘
314
315 lemma coeff_X_pow (m : σ →₀ ℕ) (s : σ) (n : ℕ) :
id ┴ └┘ ┴ ┴ ┴
src └┘ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴
doc └┘
316 coeff α m ((X s : mv_power_series σ α)^n) = if m = single s n then 1 else 0 :=
id └───┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴
src └───┘ ┴ └─────────────┘ ┴ ┴ ┴ └────┘
typ └───┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴
doc └───┘ ┴ └─────────────┘ └────┘
317 by rw [X_pow_eq s n, coeff_monomial]
id └──────┘ ┴ ┴ └────────────┘
src └──┘└──────┘┴ ┴ └┘└────────────┘└─
typ └──┘└──────┘┴┴┴┴└┘└────────────┘└─
doc └──┘ ┴ ┴ └┘ └─
txt └──┘ ┴ ┴ └┘ └─
par └──┘ ┴ ┴ └┘ └─
pid └┘ ┴ ┴ └┘ ┴└
st └───────────────┘└──────────────┘┴└
318
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
319 @[simp] lemma coeff_mul_C (n : σ →₀ ℕ) (φ : mv_power_series σ α) (a : α) :
id ┴ └┘ ┴ └─────────────┘ ┴ ┴ ┴
src └┘ ┴ └─────────────┘
typ ┴ └┘ ┴ └─────────────┘ ┴ ┴ ┴
doc └──┘ └┘ └─────────────┘
320 coeff α n (φ * (C σ α a)) = (coeff α n φ) * a :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ └───┘ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ ┴ └───┘
321 begin
st └─────
322 rw [coeff_mul n φ], rw [finset.sum_eq_single (n,(0 : σ →₀ ℕ))],
id └───────┘ ┴ ┴ └──────────────────┘ ┴┴ ┴ └┘
src └──┘└───────┘┴ ┴ ┴ └──┘└──────────────────┘┴┴ ┴ └──┘ ┴└┘┴ └─┘
typ └──┘└───────┘┴┴┴┴┴ └──┘└──────────────────┘┴┴┴┴ └──┘┴┴└┘┴ └─┘
doc └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴└┘┴ └─┘
txt └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └─┘
par └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └─┘
pid └┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴ └─┘
st ──────────────────┘└──────────────────────────────────────────┘└──
323 { rw [coeff_C, if_pos rfl] },
id └─────┘ └────┘ └─┘
src └──┘└─────┘└┘└────┘┴└─┘└┘
typ └──┘└─────┘└┘└────┘┴└─┘└┘
doc └──┘ └┘ ┴ └┘
txt └──┘ └┘ ┴ └┘
par └──┘ └┘ ┴ └┘
pid └┘ └┘ ┴ ┴┴
st ───┘└─────────┘└──────────┘┴┴└┘└
324 { rintro ⟨i,j⟩ hij hne,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └────────────┘
st ───┘└──────────────────┘└─
325 rw finsupp.mem_antidiagonal_support at hij,
id └──────────────────────────────┘
src └─┘└──────────────────────────────┘└─────┘
typ └─┘└──────────────────────────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ─────────────────────────────────────────────┘└─
326 by_cases hj : j = 0,
id ┴ ┴
src └───────┘ └─┘ ┴┴└┘
typ └───────┘ └─┘┴┴┴└┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ──────────────────────┘└─
327 { subst hj, simp at *, contradiction },
id └┘
src └────┘ └───────┘ └────────────┘
typ └────┘└┘ └───────┘ └────────────┘
doc └────┘ └───────┘ └────────────┘
txt └────┘ └───────┘ └────────────┘
par └────┘ └───────┘ └────────────┘
pid ┴ ┴└──┘ ┴
st ─────┘└──────┘└─────────┘└──────────────┘└┘└
328 { rw [coeff_C, if_neg hj, mul_zero] } },
id └─────┘ └────┘ └┘ └──────┘
src └──┘└─────┘└┘└────┘┴ └┘└──────┘└┘
typ └──┘└─────┘└┘└────┘┴└┘└┘└──────┘└┘
doc └──┘ └┘ ┴ └┘ └┘
txt └──┘ └┘ ┴ └┘ └┘
par └──┘ └┘ ┴ └┘ └┘
pid └┘ └┘ ┴ └┘ ┴┴
st ────────────────┘└─────────┘└────────┘┴┴└──┘└
329 { intro h, exfalso, apply h,
src └─────┘ └─────┘ └────┘
typ └─────┘ └─────┘ └────┘
doc └─────┘ └─────┘ └────┘
txt └─────┘ └─────┘ └────┘
par └─────┘ └─────┘ └────┘
pid └┘ ┴
st ──────────┘└───────┘└───────┘└─
330 rw finsupp.mem_antidiagonal_support,
id └──────────────────────────────┘
src └─┘└──────────────────────────────┘
typ └─┘└──────────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────────────────────┘└─
331 apply add_zero }
id └──────┘
src └────┘└──────┘┴
typ └────┘└──────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────┘└─
332 end
st ──┘
333
334 @[simp] lemma coeff_zero_mul_X (φ : mv_power_series σ α) (s : σ) :
id └─────────────┘ ┴ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴ ┴
doc └──┘ └─────────────┘
335 coeff α (0 : σ →₀ ℕ) (φ * X s) = 0 :=
id └───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └┘ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └┘ ┴
336 begin
st └─────
337 rw [coeff_mul _ φ, finset.sum_eq_zero],
id └───────┘ ┴ └────────────────┘
src └──┘└───────┘└─┘ └┘└────────────────┘┴
typ └──┘└───────┘└─┘┴└┘└────────────────┘┴
doc └──┘ └─┘ └┘ ┴
txt └──┘ └─┘ └┘ ┴
par └──┘ └─┘ └┘ ┴
pid └┘ └─┘ └┘ ┴
st ──────────────────┘└──────────────────┘└──
338 rintro ⟨i,j⟩ hij,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ─────────────────┘└─
339 obtain ⟨rfl, rfl⟩ : i = 0 ∧ j = 0,
id ┴ ┴ ┴ ┴
src └──────────────────┘ ┴┴└─┘┴┴ ┴ └┘
typ └──────────────────┘┴┴┴└─┘┴┴┴┴ └┘
doc └──────────────────┘ ┴ └─┘ ┴ ┴ └┘
txt └──────────────────┘ ┴ └─┘ ┴ ┴ └┘
par └──────────────────┘ ┴ └─┘ ┴ ┴ └┘
pid └────────────┘ ┴ └─┘ ┴ ┴ ┴┴
st ──────────────────────────────────┘└─
340 { rw finsupp.mem_antidiagonal_support at hij,
id └──────────────────────────────┘
src └─┘└──────────────────────────────┘└─────┘
typ └─┘└──────────────────────────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ───┘└────────────────────────────────────────┘└─
341 simpa using hij },
id └─┘
src └──────────┘ ┴
typ └──────────┘└─┘┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st ───────────────────┘└┘└
342 simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────┘└─
343 end
st ──┘
344
345 variables (σ) (α)
346
347 /-- The constant coefficient of a formal power series.-/
348 def constant_coeff : (mv_power_series σ α) →+* α :=
id └─────────────┘ ┴ ┴ └─┘ ┴
src └─────────────┘ └─┘
typ └─────────────┘ ┴ ┴ └─┘ ┴
doc └─────────────┘ └─┘
349 { to_fun := coeff α (0 : σ →₀ ℕ),
id └───┘ ┴ ┴ └┘ ┴
src └───┘ └┘ ┴
typ └───┘ ┴ ┴ └┘ ┴
doc └───┘ └┘
350 map_one' := coeff_zero_one,
id └────────────┘
src └────────────┘
typ └────────────┘
351 map_mul' := λ φ ψ, by simp [coeff_mul, support_single_ne_zero],
id ┴ ┴ └───────┘ └────────────────────┘
src └────┘└───────┘└┘└────────────────────┘┴
typ ┴ ┴ └────┘└───────┘└┘└────────────────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └───────────────────────────────────────┘
352 .. coeff α (0 : σ →₀ ℕ) }
id └───┘ ┴ ┴ └┘ ┴
src └───┘ └┘ ┴
typ └───┘ ┴ ┴ └┘ ┴
doc └───┘ └┘
353
354 variables {σ} {α}
355
356 @[simp] lemma coeff_zero_eq_constant_coeff :
doc └──┘
357 coeff α (0 : σ →₀ ℕ) = constant_coeff σ α := rfl
id └───┘ ┴ ┴ └┘ ┴ ┴ └────────────┘ ┴ ┴ └─┘
src └───┘ └┘ ┴ ┴ └────────────┘ └─┘
typ └───┘ ┴ ┴ └┘ ┴ ┴ └────────────┘ ┴ ┴ └─┘
doc └───┘ └┘ └────────────┘
358 @[simp] lemma coeff_zero_eq_constant_coeff_apply (φ : mv_power_series σ α) :
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
doc └──┘ └─────────────┘
359 coeff α (0 : σ →₀ ℕ) φ = constant_coeff σ α φ := rfl
id └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ └─┘
src └───┘ └┘ ┴ ┴ └────────────┘ └─┘
typ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ └─┘
doc └───┘ └┘ └────────────┘
360
361 @[simp] lemma constant_coeff_C (a : α) : constant_coeff σ α (C σ α a) = a := rfl
id ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └────────────┘ ┴ ┴ └─┘
typ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └────────────┘ ┴
362 @[simp] lemma constant_coeff_comp_C :
doc └──┘
363 (constant_coeff σ α).comp (C σ α) = ring_hom.id α := rfl
id └────────────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ └─┘
src └────────────┘ └──┘ ┴ ┴ └─────────┘ └─┘
typ └────────────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ └─┘
doc └────────────┘ └──┘ ┴ └─────────┘
364
365 @[simp] lemma constant_coeff_zero : constant_coeff σ α 0 = 0 := rfl
id └────────────┘ ┴ ┴ ┴ └─┘
src └────────────┘ ┴ └─┘
typ └────────────┘ ┴ ┴ ┴ └─┘
doc └──┘ └────────────┘
366 @[simp] lemma constant_coeff_one : constant_coeff σ α 1 = 1 := rfl
id └────────────┘ ┴ ┴ ┴ └─┘
src └────────────┘ ┴ └─┘
typ └────────────┘ ┴ ┴ ┴ └─┘
doc └──┘ └────────────┘
367 @[simp] lemma constant_coeff_X (s : σ) : constant_coeff σ α (X s) = 0 := coeff_zero_X s
id ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
src └────────────┘ ┴ ┴ └──────────┘
typ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
doc └──┘ └────────────┘ ┴
368
369 /-- If a multivariate formal power series is invertible,
370 then so is its constant coefficient.-/
371 lemma is_unit_constant_coeff (φ : mv_power_series σ α) (h : is_unit φ) :
id └─────────────┘ ┴ ┴ └─────┘ ┴
src └─────────────┘ └─────┘
typ └─────────────┘ ┴ ┴ └─────┘ ┴
doc └─────────────┘ └─────┘
372 is_unit (constant_coeff σ α φ) :=
id └─────┘ └────────────┘ ┴ ┴ ┴
src └─────┘ └────────────┘
typ └─────┘ └────────────┘ ┴ ┴ ┴
doc └─────┘ └────────────┘
373 h.map' (constant_coeff σ α)
id ┴└───┘ └────────────┘ ┴ ┴
src └───┘ └────────────┘
typ ┴└───┘ └────────────┘ ┴ ┴
doc └────────────┘
374
375 instance : semimodule α (mv_power_series σ α) :=
id └────────┘ ┴ └─────────────┘ ┴ ┴
src └────────┘ └─────────────┘
typ └────────┘ ┴ └─────────────┘ ┴ ┴
doc └────────┘ └─────────────┘
376 { smul := λ a φ, C σ α a * φ,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
377 one_smul := λ φ, one_mul _,
id ┴ └─────┘
src └─────┘
typ ┴ └─────┘
378 mul_smul := λ a b φ, by simp [ring_hom.map_mul, mul_assoc],
id ┴ ┴ ┴ └──────────────┘ └───────┘
src └────┘└──────────────┘└┘└───────┘┴
typ ┴ ┴ ┴ └────┘└──────────────┘└┘└───────┘┴
doc └────┘└──────────────┘└┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └─────────────────────────────────┘
379 smul_add := λ a φ ψ, mul_add _ _ _,
id ┴ ┴ ┴ └─────┘
src └─────┘
typ ┴ ┴ ┴ └─────┘
380 smul_zero := λ a, mul_zero _,
id ┴ └──────┘
src └──────┘
typ ┴ └──────┘
381 add_smul := λ a b φ, by simp only [ring_hom.map_add, add_mul],
id ┴ ┴ ┴ └──────────────┘ └─────┘
src └─────────┘└──────────────┘└┘└─────┘┴
typ ┴ ┴ ┴ └─────────┘└──────────────┘└┘└─────┘┴
doc └─────────┘└──────────────┘└┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └────────────────────────────────────┘
382 zero_smul := λ φ, by simp only [zero_mul, ring_hom.map_zero] }
id ┴ └──────┘ └───────────────┘
src └─────────┘└──────┘└┘└───────────────┘└┘
typ ┴ └─────────┘└──────┘└┘└───────────────┘└┘
doc └─────────┘ └┘└───────────────┘└┘
txt └─────────┘ └┘ └┘
par └─────────┘ └┘ └┘
pid ┴└──┘└┘ └┘ ┴┴
st └───────────────────────────────────────┘
383
384 end semiring
385
386 instance [ring α] : module α (mv_power_series σ α) :=
id └──┘ ┴ └────┘ ┴ └─────────────┘ ┴ ┴
src └──┘ └────┘ └─────────────┘
typ └──┘ ┴ └────┘ ┴ └─────────────┘ ┴ ┴
doc └────┘ └─────────────┘
387 { ..mv_power_series.semimodule }
id └────────────────────────┘
src └────────────────────────┘
typ └────────────────────────┘
388
389 instance [comm_ring α] : algebra α (mv_power_series σ α) :=
id └───────┘ ┴ └─────┘ ┴ └─────────────┘ ┴ ┴
src └───────┘ └─────┘ └─────────────┘
typ └───────┘ ┴ └─────┘ ┴ └─────────────┘ ┴ ┴
doc └─────┘ └─────────────┘
390 { to_fun := C σ α,
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
doc ┴
391 commutes' := λ _ _, mul_comm _ _,
id ┴ ┴ └──────┘
src └──────┘
typ ┴ ┴ └──────┘
392 smul_def' := λ c p, rfl,
id ┴ ┴ └─┘
src └─┘
typ ┴ ┴ └─┘
393 .. mv_power_series.module }
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
394
395 section map
396 variables {β : Type*} {γ : Type*} [semiring α] [semiring β] [semiring γ]
id └──────┘ └──────┘ └──────┘
src └──────┘ └──────┘ └──────┘
typ └──────┘ └──────┘ └──────┘
397 variables (f : α →+* β) (g : β →+* γ)
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
doc └─┘ └─┘
398
399 variable (σ)
400
401 /-- The map between multivariate formal power series induced by a map on the coefficients.-/
402 def map : mv_power_series σ α →+* mv_power_series σ β :=
id └─────────────┘ ┴ ┴ └─┘ └─────────────┘ ┴ ┴
src └─────────────┘ └─┘ └─────────────┘
typ └─────────────┘ ┴ ┴ └─┘ └─────────────┘ ┴ ┴
doc └─────────────┘ └─┘ └─────────────┘
403 { to_fun := λ φ n, f $ coeff α n φ,
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src └───┘
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
doc └───┘
404 map_zero' := ext $ λ n, f.map_zero,
id └─┘ ┴ ┴└───────┘
src └─┘ └───────┘
typ └─┘ ┴ ┴└───────┘
doc └─┘ └───────┘
405 map_one' := ext $ λ n, show f ((coeff α n) 1) = (coeff β n) 1,
id └─┘ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └─┘ └───┘ ┴ └───┘
typ └─┘ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
doc └─┘ └───┘ └───┘
406 by { rw [coeff_one, coeff_one], split_ifs; simp [f.map_one, f.map_zero] },
id └───────┘ └───────┘
src └──┘└───────┘└┘└───────┘┴ └───────┘ └────┘ └┘ └┘
typ └──┘└───────┘└┘└───────┘┴ └───────┘ └────┘└───────┘└┘└────────┘└┘
doc └──┘ └┘ ┴ └───────┘ └────┘ └┘ └┘
txt └──┘ └┘ ┴ └───────┘ └────┘ └┘ └┘
par └──┘ └┘ ┴ └───────┘ └────┘ └┘ └┘
pid └┘ └┘ ┴ ┴┴ └┘ ┴┴
st └──────────────┘└─────────┘└─────────────────────────────────────────┘└┘
407 map_add' := λ φ ψ, ext $ λ n,
id ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ └─┘ ┴
doc └─┘
408 show f ((coeff α n) (φ + ψ)) = f ((coeff α n) φ) + f ((coeff α n) ψ), by simp,
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src └───┘ ┴ ┴ └───┘ ┴ └───┘ └──┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘
doc └───┘ └───┘ └───┘ └──┘
txt └──┘
par └──┘
st └───┘
409 map_mul' := λ φ ψ, ext $ λ n, show f _ = _,
id ┴ ┴ └─┘ ┴ ┴ ┴
src └─┘ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘
410 begin
st └─────
411 rw [coeff_mul, ← finset.sum_hom _ f, coeff_mul, finset.sum_congr rfl],
id └───────┘ └────────────┘ ┴ └───────┘ └──────────────┘ └─┘
src └──┘└───────┘└──┘└────────────┘└─┘ └┘└───────┘└┘└──────────────┘┴└─┘┴
typ └──┘└───────┘└──┘└────────────┘└─┘┴└┘└───────┘└┘└──────────────┘┴└─┘┴
doc └──┘ └──┘ └─┘ └┘ └┘ ┴ ┴
txt └──┘ └──┘ └─┘ └┘ └┘ ┴ ┴
par └──┘ └──┘ └─┘ └┘ └┘ ┴ ┴
pid └┘ └──┘ └─┘ └┘ └┘ ┴ ┴
st ────────────────┘└────────────────────┘└─────────┘└────────────────────┘┴└─
412 rintros ⟨i,j⟩ hij, rw [f.map_mul], refl,
src └───────────────┘ └──┘
typ └───────────────┘ └──┘└───────┘
doc └───────────────┘ └──┘
txt └───────────────┘ └──┘
par └───────────────┘ └──┘
pid └────────┘ └┘
st ────────────────────┘└─────────────┘ └─
413 end }
st ────┘
414
415 variable {σ}
416
417 @[simp] lemma map_id : map σ (ring_hom.id α) = ring_hom.id _ := rfl
id └─┘ ┴ └─────────┘ ┴ ┴ └─────────┘ └─┘
src └─┘ └─────────┘ ┴ └─────────┘ └─┘
typ └─┘ ┴ └─────────┘ ┴ ┴ └─────────┘ └─┘
doc └──┘ └─┘ └─────────┘ └─────────┘
418
419 lemma map_comp : map σ (g.comp f) = (map σ g).comp (map σ f) := rfl
id └─┘ ┴ ┴└───┘ ┴ ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ └─┘
src └─┘ └───┘ ┴ └─┘ └──┘ └─┘ └─┘
typ └─┘ ┴ ┴└───┘ ┴ ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ └─┘
doc └─┘ └───┘ └─┘ └──┘ └─┘
420
421 @[simp] lemma coeff_map (n : σ →₀ ℕ) (φ : mv_power_series σ α) :
id ┴ └┘ ┴ └─────────────┘ ┴ ┴
src └┘ ┴ └─────────────┘
typ ┴ └┘ ┴ └─────────────┘ ┴ ┴
doc └──┘ └┘ └─────────────┘
422 coeff β n (map σ f φ) = f (coeff α n φ) := rfl
id └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─┘
src └───┘ └─┘ ┴ └───┘ └─┘
typ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─┘
doc └───┘ └─┘ └───┘
423
424 @[simp] lemma constant_coeff_map (φ : mv_power_series σ α) :
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
doc └──┘ └─────────────┘
425 constant_coeff σ β (map σ f φ) = f (constant_coeff σ α φ) := rfl
id └────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ └─┘
src └────────────┘ └─┘ ┴ └────────────┘ └─┘
typ └────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ └─┘
doc └────────────┘ └─┘ └────────────┘
426
427 end map
428
429 section trunc
430 variables [comm_semiring α] (n : σ →₀ ℕ)
id └───────────┘ └┘ ┴
src └───────────┘ └┘ ┴
typ └───────────┘ └┘ ┴
doc └┘
431
432 -- Auxiliary definition for the truncation function.
433 def trunc_fun (φ : mv_power_series σ α) : mv_polynomial σ α :=
id └─────────────┘ ┴ ┴ └───────────┘ ┴ ┴
src └─────────────┘ └───────────┘
typ └─────────────┘ ┴ ┴ └───────────┘ ┴ ┴
doc └─────────────┘ └───────────┘
434 { support := (n.antidiagonal.support.image prod.fst).filter (λ m, coeff α m φ ≠ 0),
id ┴└───────────┘└──────┘└────┘ └──────┘ └────┘ ┴ └───┘ ┴ ┴ ┴ ┴
src └───────────┘└──────┘└────┘ └──────┘ └────┘ └───┘ ┴
typ ┴└───────────┘└──────┘└────┘ └──────┘ └────┘ ┴ └───┘ ┴ ┴ ┴ ┴
doc └────┘ └────┘ └───┘
435 to_fun := λ m, if m ≤ n then coeff α m φ else 0,
id ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src ┴ └───┘
typ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
doc └───┘
436 mem_support_to_fun := λ m,
id ┴
typ ┴
437 begin
st └───┘
438 suffices : m ∈ finset.image prod.fst ((antidiagonal n).support) ↔ m ≤ n,
id ┴
src ┴
typ ┴
439 { rw [finset.mem_filter, this], split,
440 { intro h, rw [if_pos h.1], exact h.2 },
st └┘
441 { intro h, split_ifs at h with H H,
442 { exact ⟨H, h⟩ },
st └┘
443 { exfalso, exact h rfl } } },
st └────┘
444 rw finset.mem_image, split,
445 { rintros ⟨⟨i,j⟩, h, rfl⟩ s,
446 rw finsupp.mem_antidiagonal_support at h,
447 rw ← h, exact nat.le_add_right _ _ },
st └┘
448 { intro h, refine ⟨(m, n-m), _, rfl⟩,
id ┴
typ ┴
449 rw finsupp.mem_antidiagonal_support, ext s, exact nat.add_sub_of_le (h s) }
id ┴
typ ┴
st └┘
450 end }
st └─┘
451
452 variable (α)
453
454 /-- The `n`th truncation of a multivariate formal power series to a multivariate polynomial -/
455 def trunc : mv_power_series σ α →+ mv_polynomial σ α :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
456 { to_fun := trunc_fun n,
id ┴
typ ┴
457 map_zero' := mv_polynomial.ext _ _ $ λ m, by { change ite _ _ _ = _, split_ifs; refl },
id ┴ └──┘
src └──┘
typ ┴ └──┘
doc └──┘
st └┘
458 map_add' := λ φ ψ, mv_polynomial.ext _ _ $ λ m,
id ┴ ┴ ┴
typ ┴ ┴ ┴
459 begin
460 rw mv_polynomial.coeff_add,
461 change ite _ _ _ = ite _ _ _ + ite _ _ _,
462 split_ifs with H, {refl}, {rw [zero_add]}
st └┘ └─┘
463 end }
st └─┘
464
465 variable {α}
466
467 lemma coeff_trunc (m : σ →₀ ℕ) (φ : mv_power_series σ α) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
468 mv_polynomial.coeff m (trunc α n φ) =
id ┴ ┴ ┴
typ ┴ ┴ ┴
469 if m ≤ n then coeff α m φ else 0 := rfl
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
470
471 @[simp] lemma trunc_one : trunc α n 1 = 1 :=
id ┴ ┴
typ ┴ ┴
doc └──┘
472 mv_polynomial.ext _ _ $ λ m,
id ┴
typ ┴
473 begin
474 rw [coeff_trunc, coeff_one],
475 split_ifs with H H' H',
476 { subst m, erw mv_polynomial.coeff_C 0, simp },
id ┴
typ ┴
st └┘
477 { symmetry, erw mv_polynomial.coeff_monomial, convert if_neg (ne.elim (ne.symm H')), },
st └┘
478 { symmetry, erw mv_polynomial.coeff_monomial, convert if_neg _,
479 intro H', apply H, subst m, intro s, exact nat.zero_le _ }
id ┴
typ ┴
st └─
480 end
st ──┘
481
482 @[simp] lemma trunc_C (a : α) : trunc α n (C σ α a) = mv_polynomial.C a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
483 mv_polynomial.ext _ _ $ λ m,
id ┴
typ ┴
484 begin
485 rw [coeff_trunc, coeff_C, mv_polynomial.coeff_C],
486 split_ifs with H; refl <|> try {simp * at *},
id └──┘ └─┘
src └──┘ └─┘
typ └──┘ └─┘
doc └──┘ └─┘
st └┘
487 exfalso, apply H, subst m, intro s, exact nat.zero_le _
id ┴
typ ┴
488 end
st └─┘
489
490 end trunc
491
492 section comm_semiring
493 variable [comm_semiring α]
id └┘ └───┘ └─┘
src └┘ └───┘ └─┘
typ └┘ └───┘ └─┘
494
495 lemma X_pow_dvd_iff {s : σ} {n : ℕ} {φ : mv_power_series σ α} :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
496 (X s : mv_power_series σ α)^n ∣ φ ↔ ∀ m : σ →₀ ℕ, m s < n → coeff α m φ = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
497 begin
498 split,
499 { rintros ⟨φ, rfl⟩ m h,
500 rw [coeff_mul, finset.sum_eq_zero],
501 rintros ⟨i,j⟩ hij, rw [coeff_X_pow, if_neg, zero_mul],
502 contrapose! h, subst i, rw finsupp.mem_antidiagonal_support at hij,
id ┴
typ ┴
503 rw [← hij, finsupp.add_apply, finsupp.single_eq_same], exact nat.le_add_right n _ },
id ┴
typ ┴
st └┘
504 { intro h, refine ⟨λ m, coeff α (m + (single s n)) φ, _⟩,
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
505 ext m, by_cases H : m - single s n + single s n = m,
id ┴ ┴
typ ┴ ┴
506 { rw [coeff_mul, finset.sum_eq_single (single s n, m - single s n)],
id ┴ ┴ ┴
typ ┴ ┴ ┴
507 { rw [coeff_X_pow, if_pos rfl, one_mul],
508 simpa using congr_arg (λ (m : σ →₀ ℕ), coeff α m φ) H.symm },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
509 { rintros ⟨i,j⟩ hij hne, rw finsupp.mem_antidiagonal_support at hij,
510 rw coeff_X_pow, split_ifs with hi,
511 { exfalso, apply hne, rw [← hij, ← hi, prod.mk.inj_iff], refine ⟨rfl, _⟩,
512 ext t, simp only [nat.add_sub_cancel_left, finsupp.add_apply, finsupp.nat_sub_apply] },
st └┘
513 { exact zero_mul _ } },
st └──┘
514 { intro hni, exfalso, apply hni, rwa [finsupp.mem_antidiagonal_support, add_comm] } },
st └──┘
515 { rw [h, coeff_mul, finset.sum_eq_zero],
516 { rintros ⟨i,j⟩ hij, rw finsupp.mem_antidiagonal_support at hij,
517 rw coeff_X_pow, split_ifs with hi,
518 { exfalso, apply H, rw [← hij, hi], ext t,
519 simp only [nat.add_sub_cancel_left, add_comm,
520 finsupp.add_apply, add_right_inj, finsupp.nat_sub_apply] },
st └┘
521 { exact zero_mul _ } },
st └──┘
522 { classical, contrapose! H, ext t,
523 by_cases hst : s = t,
id ┴ ┴
typ ┴ ┴
524 { subst t, simpa using nat.add_sub_cancel' H },
id ┴
typ ┴
st └┘
525 { simp [finsupp.single_apply, hst] } } } }
id └─┘
typ └─┘
st └───────
526 end
st ──┘
527
528 lemma X_dvd_iff {s : σ} {φ : mv_power_series σ α} :
id ┴ ┴ ┴
typ ┴ ┴ ┴
529 (X s : mv_power_series σ α) ∣ φ ↔ ∀ m : σ →₀ ℕ, m s = 0 → coeff α m φ = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
530 begin
531 rw [← pow_one (X s : mv_power_series σ α), X_pow_dvd_iff],
532 split; intros h m hm,
533 { exact h m (hm.symm ▸ zero_lt_one) },
id ┴
typ ┴
st └┘
534 { exact h m (nat.eq_zero_of_le_zero $ nat.le_of_succ_le_succ hm) }
id ┴
typ ┴
st └─
535 end
st ──┘
536 end comm_semiring
537
538 section ring
539 variables [ring α]
id └┘ ┴
src └┘ ┴
typ └┘ ┴
540
541 /-
542 The inverse of a multivariate formal power series is defined by
543 well-founded recursion on the coeffients of the inverse.
544 -/
545
546 /-- Auxiliary definition that unifies
547 the totalised inverse formal power series `(_)⁻¹` and
548 the inverse formal power series that depends on
549 an inverse of the constant coefficient `inv_of_unit`.-/
550 protected noncomputable def inv.aux (a : α) (φ : mv_power_series σ α) : mv_power_series σ α
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
551 | n := if n = 0 then a else
id ┴
typ ┴
552 - a * n.antidiagonal.support.sum (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
553 if h : x.2 < n then coeff α x.1 φ * inv.aux x.2 else 0)
id ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ └┘
554 using_well_founded
555 { rel_tac := λ _ _, `[exact ⟨_, finsupp.lt_wf σ⟩],
id ┴ ┴
typ ┴ ┴
556 dec_tac := tactic.assumption }
id └───────────────┘
src └───────────────┘
typ └───────────────┘
557
558 lemma coeff_inv_aux (n : σ →₀ ℕ) (a : α) (φ : mv_power_series σ α) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
559 coeff α n (inv.aux a φ) = if n = 0 then a else
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
560 - a * n.antidiagonal.support.sum (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
561 if x.2 < n then coeff α x.1 φ * coeff α x.2 (inv.aux a φ) else 0) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
562 show inv.aux a φ n = _, by { rw inv.aux, refl }
id ┴
typ ┴
st └┘
563
564 /-- A multivariate formal power series is invertible if the constant coefficient is invertible.-/
565 def inv_of_unit (φ : mv_power_series σ α) (u : units α) : mv_power_series σ α :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
566 inv.aux (↑u⁻¹) φ
id ┴
typ ┴
567
568 lemma coeff_inv_of_unit (n : σ →₀ ℕ) (φ : mv_power_series σ α) (u : units α) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
569 coeff α n (inv_of_unit φ u) = if n = 0 then ↑u⁻¹ else
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
570 - ↑u⁻¹ * n.antidiagonal.support.sum (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
571 if x.2 < n then coeff α x.1 φ * coeff α x.2 (inv_of_unit φ u) else 0) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
572 coeff_inv_aux n (↑u⁻¹) φ
573
574 @[simp] lemma constant_coeff_inv_of_unit (φ : mv_power_series σ α) (u : units α) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
doc └──┘
575 constant_coeff σ α (inv_of_unit φ u) = ↑u⁻¹ :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
576 by rw [← coeff_zero_eq_constant_coeff_apply, coeff_inv_of_unit, if_pos rfl]
st ┴
577
578 lemma mul_inv_of_unit (φ : mv_power_series σ α) (u : units α) (h : constant_coeff σ α φ = u) :
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
579 φ * inv_of_unit φ u = 1 :=
id ┴ ┴
typ ┴ ┴
580 ext $ λ n, if H : n = 0 then by { rw H, simp [coeff_mul, support_single_ne_zero, h], }
id ┴
typ ┴
st └┘
581 else
582 begin
583 have : ((0 : σ →₀ ℕ), n) ∈ n.antidiagonal.support,
id ┴
typ ┴
584 { rw [finsupp.mem_antidiagonal_support, zero_add] },
st ┴ └┘
585 rw [coeff_one, if_neg H, coeff_mul,
586 ← finset.insert_erase this, finset.sum_insert (finset.not_mem_erase _ _),
587 coeff_zero_eq_constant_coeff_apply, h, coeff_inv_of_unit, if_neg H,
588 neg_mul_eq_neg_mul_symm, mul_neg_eq_neg_mul_symm, units.mul_inv_cancel_left,
589 ← finset.insert_erase this, finset.sum_insert (finset.not_mem_erase _ _),
590 finset.insert_erase this, if_neg (not_lt_of_ge $ le_refl _), zero_add, add_comm,
591 ← sub_eq_add_neg, sub_eq_zero, finset.sum_congr rfl],
592 rintros ⟨i,j⟩ hij, rw [finset.mem_erase, finsupp.mem_antidiagonal_support] at hij,
593 cases hij with h₁ h₂,
594 subst n, rw if_pos,
id ┴
typ ┴
595 suffices : (0 : _) + j < i + j, {simpa},
id ┴
typ ┴
st └┘
596 apply add_lt_add_right,
597 split,
598 { intro s, exact nat.zero_le _ },
st └┘
599 { intro H, apply h₁,
600 suffices : i = 0, {simp [this]},
id ┴
typ ┴
st └┘
601 ext1 s, exact nat.eq_zero_of_le_zero (H s) }
id ┴
typ ┴
st └┘
602 end
603
604 end ring
605
606 section comm_ring
607 variable [comm_ring α]
id └──┘ └─┘
src └──┘ └─┘
typ └──┘ └─┘
608
609 /-- Multivariate formal power series over a local ring form a local ring.-/
610 lemma is_local_ring (h : is_local_ring α) : is_local_ring (mv_power_series σ α) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
611 begin
612 split,
613 { have H : (0:α) ≠ 1 := ‹is_local_ring α›.1, contrapose! H,
id ┴ ┴
typ ┴ ┴
614 simpa using congr_arg (constant_coeff σ α) H },
id ┴ ┴
typ ┴ ┴
st └┘
615 { intro φ, rcases ‹is_local_ring α›.2 (constant_coeff σ α φ) with ⟨u,h⟩|⟨u,h⟩; [left, right];
id ┴ ┴ ┴ └──┘ └───┘
src └──┘ └───┘
typ ┴ ┴ ┴ └──┘ └───┘
doc └──┘ └───┘
616 { refine is_unit_of_mul_one _ _ (mul_inv_of_unit _ u _),
617 simpa using h } }
st └───
618 end
st ──┘
619
620 -- TODO(jmc): once adic topology lands, show that this is complete
621
622 end comm_ring
623
624 section nonzero_comm_ring
625 variables [nonzero_comm_ring α]
id └┘ └──┘ └──┘ ┴
src └┘ └──┘ └──┘ ┴
typ └┘ └──┘ └──┘ ┴
doc └┘ └──┘ └──┘ ┴
626
627 instance : nonzero_comm_ring (mv_power_series σ α) :=
id ┴ ┴
typ ┴ ┴
628 { zero_ne_one := assume h, zero_ne_one $ show (0:α) = 1, from congr_arg (constant_coeff σ α) h,
id ┴ ┴ ┴
typ ┴ ┴ ┴
629 .. mv_power_series.comm_ring }
630
631 lemma X_inj {s t : σ} : (X s : mv_power_series σ α) = X t ↔ s = t :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
632 ⟨begin
633 intro h, replace h := congr_arg (coeff α (single s 1)) h, rw [coeff_X, if_pos rfl, coeff_X] at h,
id ┴ ┴
typ ┴ ┴
634 split_ifs at h with H,
635 { rw finsupp.single_eq_single_iff at H,
636 cases H, { exact H.1 }, { exfalso, exact one_ne_zero H.1 } },
st └┘ └──┘
637 { exfalso, exact one_ne_zero h }
st └─
638 end, congr_arg X⟩
st ──┘
639
640 end nonzero_comm_ring
641
642 section local_ring
643 variables {β : Type*} [local_ring α] [local_ring β] (f : α →+* β) [is_local_ring_hom f]
id └┘ └──┘ └──┘ └┘
src └┘ └──┘ └──┘ └┘
typ └┘ └──┘ └──┘ └┘
644
645 instance : local_ring (mv_power_series σ α) :=
id ┴ ┴
typ ┴ ┴
646 local_of_is_local_ring $ is_local_ring ⟨zero_ne_one, local_ring.is_local⟩
647
648 instance map.is_local_ring_hom :
649 is_local_ring_hom (map σ f : mv_power_series σ α → mv_power_series σ β) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
650 { map_one := (map σ f).map_one,
id ┴
typ ┴
651 map_mul := (map σ f).map_mul,
id ┴
typ ┴
652 map_add := (map σ f).map_add,
id ┴
typ ┴
653 map_nonunit :=
654 begin
655 rintros φ ⟨ψ, h⟩,
656 replace h := congr_arg (constant_coeff σ β) h,
id ┴ ┴
typ ┴ ┴
657 rw constant_coeff_map at h,
658 have : is_unit (constant_coeff σ β ↑ψ) := @is_unit_constant_coeff σ β _ (↑ψ) (is_unit_unit ψ),
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
659 rw ← h at this,
660 rcases is_unit_of_map_unit f _ this with ⟨c, hc⟩,
661 exact is_unit_of_mul_one φ (inv_of_unit φ c) (mul_inv_of_unit φ c hc)
662 end }
st └─┘
663
664 end local_ring
665
666 section discrete_field
667 variables [discrete_field α]
id └┘ └──┘ └──┘
src └┘ └──┘ └──┘
typ └┘ └──┘ └──┘
668
669 protected def inv (φ : mv_power_series σ α) : mv_power_series σ α :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
670 inv.aux (constant_coeff σ α φ)⁻¹ φ
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
671
672 instance : has_inv (mv_power_series σ α) := ⟨mv_power_series.inv⟩
id ┴ ┴
typ ┴ ┴
673
674 lemma coeff_inv (n : σ →₀ ℕ) (φ : mv_power_series σ α) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
675 coeff α n (φ⁻¹) = if n = 0 then (constant_coeff σ α φ)⁻¹ else
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
676 - (constant_coeff σ α φ)⁻¹ * n.antidiagonal.support.sum (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
677 if x.2 < n then coeff α x.1 φ * coeff α x.2 (φ⁻¹) else 0) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
678 coeff_inv_aux n _ φ
679
680 @[simp] lemma constant_coeff_inv (φ : mv_power_series σ α) :
id ┴ ┴
typ ┴ ┴
doc └──┘
681 constant_coeff σ α (φ⁻¹) = (constant_coeff σ α φ)⁻¹ :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
682 by rw [← coeff_zero_eq_constant_coeff_apply, coeff_inv, if_pos rfl]
st ┴
683
684 lemma inv_eq_zero {φ : mv_power_series σ α} :
id ┴ ┴
typ ┴ ┴
685 φ⁻¹ = 0 ↔ constant_coeff σ α φ = 0 :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
686 ⟨λ h, by simpa using congr_arg (constant_coeff σ α) h,
id ┴ ┴
typ ┴ ┴
687 λ h, ext $ λ n, by { rw coeff_inv, split_ifs;
id ┴
typ ┴
688 simp only [h, mv_power_series.coeff_zero, zero_mul, inv_zero, neg_zero] }⟩
st └┘
689
690 @[simp] lemma inv_of_unit_eq (φ : mv_power_series σ α) (h : constant_coeff σ α φ ≠ 0) :
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
691 inv_of_unit φ (units.mk0 _ h) = φ⁻¹ := rfl
id ┴ ┴
typ ┴ ┴
692
693 @[simp] lemma inv_of_unit_eq' (φ : mv_power_series σ α) (u : units α) (h : constant_coeff σ α φ = u) :
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
694 inv_of_unit φ u = φ⁻¹ :=
id ┴ ┴
typ ┴ ┴
695 begin
696 rw ← inv_of_unit_eq φ (h.symm ▸ u.ne_zero),
697 congr' 1, rw [units.ext_iff], exact h.symm,
698 end
st └─┘
699
700 @[simp] protected lemma mul_inv (φ : mv_power_series σ α) (h : constant_coeff σ α φ ≠ 0) :
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
701 φ * φ⁻¹ = 1 :=
id ┴ ┴
typ ┴ ┴
702 by rw [← inv_of_unit_eq φ h, mul_inv_of_unit φ (units.mk0 _ h) rfl]
703
704 @[simp] protected lemma inv_mul (φ : mv_power_series σ α) (h : constant_coeff σ α φ ≠ 0) :
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
705 φ⁻¹ * φ = 1 :=
id ┴ ┴
typ ┴ ┴
706 by rw [mul_comm, φ.mul_inv h]
707
708 end discrete_field
709
710 end mv_power_series
711
712 namespace mv_polynomial
713 open finsupp
714 variables {σ : Type*} {α : Type*} [comm_semiring α]
id └┘ └┘ └┘
src └┘ └┘ └┘
typ └┘ └┘ └┘
715
716 /-- The natural inclusion from multivariate polynomials into multivariate formal power series.-/
717 instance coe_to_mv_power_series : has_coe (mv_polynomial σ α) (mv_power_series σ α) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
718 ⟨λ φ n, coeff n φ⟩
id ┴ ┴
typ ┴ ┴
719
720 @[simp, elim_cast] lemma coeff_coe (φ : mv_polynomial σ α) (n : σ →₀ ℕ) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
doc └──┘ └───────┘
721 mv_power_series.coeff α n ↑φ = coeff n φ := rfl
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
722
723 @[simp, elim_cast] lemma coe_monomial (n : σ →₀ ℕ) (a : α) :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
doc └──┘ └───────┘
724 (monomial n a : mv_power_series σ α) = mv_power_series.monomial α n a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
725 mv_power_series.ext $ λ m,
id ┴
typ ┴
726 begin
727 rw [coeff_coe, coeff_monomial, mv_power_series.coeff_monomial],
728 split_ifs with h₁ h₂; refl <|> subst m; contradiction
id └──┘ └───────────┘
src └──┘ └───────────┘
typ └──┘ └───────────┘
doc └──┘ └───────────┘
729 end
st └─┘
730
731 @[simp, elim_cast] lemma coe_zero : ((0 : mv_polynomial σ α) : mv_power_series σ α) = 0 := rfl
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘ └───────┘
732
733 @[simp, elim_cast] lemma coe_one : ((1 : mv_polynomial σ α) : mv_power_series σ α) = 1 :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘ └───────┘
734 coe_monomial _ _
735
736 @[simp, elim_cast] lemma coe_add (φ ψ : mv_polynomial σ α) :
id ┴ ┴
typ ┴ ┴
doc └──┘ └───────┘
737 ((φ + ψ : mv_polynomial σ α) : mv_power_series σ α) = φ + ψ := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
738
739 @[simp, elim_cast] lemma coe_mul (φ ψ : mv_polynomial σ α) :
id ┴ ┴
typ ┴ ┴
doc └──┘ └───────┘
740 ((φ * ψ : mv_polynomial σ α) : mv_power_series σ α) = φ * ψ :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
741 mv_power_series.ext $ λ n,
id ┴
typ ┴
742 by simp only [coeff_coe, mv_power_series.coeff_mul, coeff_mul]
743
744 @[simp, elim_cast] lemma coe_C (a : α) :
id ┴
typ ┴
doc └──┘ └───────┘
745 ((C a : mv_polynomial σ α) : mv_power_series σ α) = mv_power_series.C σ α a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
746 coe_monomial _ _
747
748 @[simp, elim_cast] lemma coe_X (s : σ) :
id ┴
typ ┴
doc └──┘ └───────┘
749 ((X s : mv_polynomial σ α) : mv_power_series σ α) = mv_power_series.X s :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
750 coe_monomial _ _
751
752 namespace coe_to_mv_power_series
753
754 instance : is_semiring_hom (coe : mv_polynomial σ α → mv_power_series σ α) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
755 { map_zero := coe_zero,
756 map_one := coe_one,
757 map_add := coe_add,
758 map_mul := coe_mul }
759
760 end coe_to_mv_power_series
761
762 end mv_polynomial
763
764 /-- Formal power series over the coefficient ring `α`.-/
765 def power_series (α : Type*) := mv_power_series unit α
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘
766
767 namespace power_series
768 open finsupp (single)
769 variable {α : Type*}
id ┴
typ ┴
770
771 instance [inhabited α] : inhabited (power_series α) := by delta power_series; apply_instance
id └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴ └────────────┘
src └┘ └┘ └┘ └┘ └┘ └┘ └────────────┘
typ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴ └────────────┘
doc └┘ └┘ └┘ └────────────┘
772 instance [add_monoid α] : add_monoid (power_series α) := by delta power_series; apply_instance
id └──┘ └──┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
src └──┘ └──┘ └┘ └┘ └┘ └┘ └┘ └────────────┘
typ └──┘ └──┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
doc └┘ └┘ └┘ └────────────┘
773 instance [add_group α] : add_group (power_series α) := by delta power_series; apply_instance
id └──┘ └─┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
src └──┘ └─┘ └┘ └┘ └┘ └┘ └┘ └────────────┘
typ └──┘ └─┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
doc └┘ └┘ └┘ └────────────┘
774 instance [add_comm_monoid α] : add_comm_monoid (power_series α) := by delta power_series; apply_instance
id └──┘ └──┘ └─┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └────────────┘
src └──┘ └──┘ └─┘ └┘ └┘ └┘ ┴ ┴ └┘ └┘ ┴ └────────────┘
typ └──┘ └──┘ └─┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └────────────┘
doc ┴ └┘ └┘ ┴ └────────────┘
775 instance [add_comm_group α] : add_comm_group (power_series α) := by delta power_series; apply_instance
id └──┘ └──┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
src └──┘ └──┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └────────────┘
typ └──┘ └──┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
doc └┘ └┘ └┘ └────────────┘
776 instance [semiring α] : semiring (power_series α) := by delta power_series; apply_instance
id └──┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
src └──┘ └┘ └┘ └┘ └┘ └┘ └┘ └────────────┘
typ └──┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
doc └┘ └┘ └┘ └────────────┘
777 instance [comm_semiring α] : comm_semiring (power_series α) := by delta power_series; apply_instance
id └──┘ └──┘ ┴ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
src └──┘ └──┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └────────────┘
typ └──┘ └──┘ ┴ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
doc └┘ └┘ └┘ └────────────┘
778 instance [ring α] : ring (power_series α) := by delta power_series; apply_instance
id └──┘ ┴ ┴ ┴ └┘ └┘ └┘ ┴ └────────────┘
src └──┘ ┴ ┴ └┘ └┘ └┘ └────────────┘
typ └──┘ ┴ ┴ ┴ └┘ └┘ └┘ ┴ └────────────┘
doc └┘ └┘ └┘ └────────────┘
779 instance [comm_ring α] : comm_ring (power_series α) := by delta power_series; apply_instance
id └──┘ └─┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
src └──┘ └─┘ └┘ └┘ └┘ └┘ └┘ └────────────┘
typ └──┘ └─┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
doc └┘ └┘ └┘ └────────────┘
780 instance [nonzero_comm_ring α] : nonzero_comm_ring (power_series α) := by delta power_series; apply_instance
id └──┘ └──┘ └──┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
src └──┘ └──┘ └──┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └────────────┘
typ └──┘ └──┘ └──┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └────────────┘
doc └──┘ └──┘ └──┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └────────────┘
781 instance [semiring α] : semimodule α (power_series α) := by delta power_series; apply_instance
id └──┘ └┘ ┴ ┴ └─┘ └┘ └┘ ┴ └────────────┘
src └──┘ └┘ └─┘ └┘ └┘ └────────────┘
typ └──┘ └┘ ┴ ┴ └─┘ └┘ └┘ ┴ └────────────┘
doc └─┘ └┘ └┘ └────────────┘
782 instance [ring α] : module α (power_series α) := by delta power_series; apply_instance
id └──┘ ┴ ┴ └┘ └┘ └┘ ┴ └────────────┘
src └──┘ └┘ └┘ └┘ └────────────┘
typ └──┘ ┴ ┴ └┘ └┘ └┘ ┴ └────────────┘
doc └┘ └┘ └┘ └────────────┘
783 instance [comm_ring α] : algebra α (power_series α) := by delta power_series; apply_instance
id └──┘ └─┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └────────────┘
src └──┘ └─┘ ┴ └┘ └┘ ┴ └────────────┘
typ └──┘ └─┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └────────────┘
doc ┴ └┘ └┘ ┴ └────────────┘
784
785 section add_monoid
786 variables (α) [add_monoid α]
id └──┘ └──┘
src └──┘ └──┘
typ └──┘ └──┘
787
788 /-- The `n`th coefficient of a formal power series.-/
789 def coeff (n : ℕ) : power_series α →+ α := mv_power_series.coeff α (single () n)
id ┴ └┘ └┘ └┘ ┴ ┴ ┴ └┘ ┴
src ┴ └┘ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴ ┴ ┴ └┘ ┴
doc └┘ └┘ └┘
790
791 /-- The `n`th monomial with coefficient `a` as formal power series.-/
792 def monomial (n : ℕ) : α →+ power_series α := mv_power_series.monomial α (single () n)
id ┴ ┴ └┘ └┘ └┘ ┴ ┴ └┘ ┴
src ┴ └┘ └┘ └┘ └┘
typ ┴ ┴ └┘ └┘ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘ └┘
793
794 variables {α}
795
796 lemma coeff_def {s : unit →₀ ℕ} {n : ℕ} (h : s () = n) :
id └──┘ ┴ ┴ ┴ └┘ ┴
src └──┘ ┴ ┴ └┘
typ └──┘ ┴ ┴ ┴ └┘ ┴
doc └──┘
797 coeff α n = mv_power_series.coeff α s :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
798 by erw [coeff, ← h, ← finsupp.unique_single s]
id ┴
typ ┴
st ┴
799
800 /-- Two formal power series are equal if all their coefficients are equal.-/
801 @[ext] lemma ext {φ ψ : power_series α} (h : ∀ n, coeff α n φ = coeff α n ψ) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
802 φ = ψ :=
id ┴ ┴
typ ┴ ┴
803 mv_power_series.ext $ λ n,
id ┴
typ ┴
804 by { rw ← coeff_def, { apply h }, refl }
st └┘ └┘
805
806 /-- Two formal power series are equal if all their coefficients are equal.-/
807 lemma ext_iff {φ ψ : power_series α} : φ = ψ ↔ (∀ n, coeff α n φ = coeff α n ψ) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
808 ⟨λ h n, congr_arg (coeff α n) h, ext⟩
id ┴ ┴ ┴
typ ┴ ┴ ┴
809
810 /-- Constructor for formal power series.-/
811 def mk (f : ℕ → α) : power_series α := λ s, f (s ())
id ┴ ┴ └┘ └┘ └┘ ┴ ┴ └┘
src ┴ └┘ └┘ └┘ └┘
typ ┴ ┴ └┘ └┘ └┘ ┴ ┴ └┘
doc └┘ └┘ └┘
812
813 @[simp] lemma coeff_mk (n : ℕ) (f : ℕ → α) : coeff α n (mk f) = f n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
814 congr_arg f finsupp.single_eq_same
id ┴
typ ┴
815
816 lemma coeff_monomial (m n : ℕ) (a : α) :
id ┴
typ ┴
817 coeff α m (monomial α n a) = if m = n then a else 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
818 calc coeff α m (monomial α n a) = _ : mv_power_series.coeff_monomial _ _ _
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
819 ... = if m = n then a else 0 :
id ┴ ┴ ┴
typ ┴ ┴ ┴
820 by { simp only [finsupp.unique_single_eq_iff], split_ifs; refl }
id └──┘
src └──┘
typ └──┘
doc └──┘
st └┘
821
822 lemma monomial_eq_mk (n : ℕ) (a : α) :
id ┴ ┴
src ┴
typ ┴ ┴
823 monomial α n a = mk (λ m, if m = n then a else 0) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
824 ext $ λ m, by { rw [coeff_monomial, coeff_mk] }
id ┴
typ ┴
st ┴ └┘
825
826 @[simp] lemma coeff_monomial' (n : ℕ) (a : α) :
id ┴ ┴
src ┴
typ ┴ ┴
doc └──┘
827 coeff α n (monomial α n a) = a :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
828 by convert if_pos rfl
829
830 @[simp] lemma coeff_comp_monomial (n : ℕ) :
id ┴
src ┴
typ ┴
doc └──┘
831 (coeff α n).comp (monomial α n) = add_monoid_hom.id α :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
832 add_monoid_hom.ext $ coeff_monomial' n
id ┴
typ ┴
833
834 end add_monoid
835
836 section semiring
837 variable [semiring α]
id ┴ └──┘
src ┴ └──┘
typ ┴ └──┘
838
839 variable (α)
840
841 /--The constant coefficient of a formal power series. -/
842 def constant_coeff : power_series α →+* α := mv_power_series.constant_coeff unit α
id └┘ └┘ └┘ ┴ ┴ └──┘ ┴
src └┘ └┘ └┘ └──┘
typ └┘ └┘ └┘ ┴ ┴ └──┘ ┴
doc └┘ └┘ └┘ └──┘
843
844 /-- The constant formal power series.-/
845 def C : α →+* power_series α := mv_power_series.C unit α
id ┴ └┘ └┘ └┘ ┴ └──┘ ┴
src └┘ └┘ └┘ └──┘
typ ┴ └┘ └┘ └┘ ┴ └──┘ ┴
doc └┘ └┘ └┘ └──┘
846
847 variable {α}
848
849 /-- The variable of the formal power series ring.-/
850 def X : power_series α := mv_power_series.X ()
id └┘ └┘ └┘ ┴ └┘
src └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ └┘
doc └┘ └┘ └┘
851
852 @[simp] lemma coeff_zero_eq_constant_coeff :
doc └──┘
853 coeff α 0 = constant_coeff α :=
id ┴ ┴
typ ┴ ┴
854 begin
855 rw [constant_coeff, ← mv_power_series.coeff_zero_eq_constant_coeff, coeff_def], refl
856 end
st └─┘
857
858 @[simp] lemma coeff_zero_eq_constant_coeff_apply (φ : power_series α) :
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └──┘ └┘ └┘ └┘
859 coeff α 0 φ = constant_coeff α φ :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
860 by rw [coeff_zero_eq_constant_coeff]; refl
id └──┘
src └──┘
typ └──┘
doc └──┘
861
862 @[simp] lemma monomial_zero_eq_C : monomial α 0 = C α :=
id ┴ ┴
typ ┴ ┴
doc └──┘
863 by rw [monomial, finsupp.single_zero, mv_power_series.monomial_zero_eq_C, C]
st ┴
864
865 @[simp] lemma monomial_zero_eq_C_apply (a : α) : monomial α 0 a = C α a :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
866 by rw [monomial_zero_eq_C]; refl
id └──┘
src └──┘
typ └──┘
doc └──┘
867
868 lemma coeff_C (n : ℕ) (a : α) :
id ┴ ┴
src ┴
typ ┴ ┴
869 coeff α n (C α a : power_series α) = if n = 0 then a else 0 :=
id ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴ ┴ ┴
src └┘ └┘ └┘
typ ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴ ┴ ┴
doc └┘ └┘ └┘
870 by rw [← monomial_zero_eq_C_apply, coeff_monomial]
871
872 @[simp] lemma coeff_zero_C (a : α) : coeff α 0 (C α a) = a :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
873 by rw [← monomial_zero_eq_C_apply, coeff_monomial' 0 a]
874
875 lemma X_eq : (X : power_series α) = monomial α 1 1 := rfl
id └┘ └┘ └┘ ┴ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴
doc └┘ └┘ └┘
876
877 lemma coeff_X (n : ℕ) :
id ┴
src ┴
typ ┴
878 coeff α n (X : power_series α) = if n = 1 then 1 else 0 :=
id ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴
src ┴ └┘ └┘ ┴
typ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴
doc ┴ └┘ └┘ ┴
879 by rw [X_eq, coeff_monomial]
880
881 @[simp] lemma coeff_zero_X : coeff α 0 (X : power_series α) = 0 :=
id ┴ ┴ └┘ └┘ ┴ ┴
src ┴ └┘ └┘ ┴
typ ┴ ┴ └┘ └┘ ┴ ┴
doc └──┘ ┴ └┘ └┘ ┴
882 by rw [coeff, finsupp.single_zero, X, mv_power_series.coeff_zero_X]
st ┴
883
884 @[simp] lemma coeff_one_X : coeff α 1 (X : power_series α) = 1 :=
id ┴ ┴ └┘ └┘ ┴ ┴
src ┴ └┘ └┘ ┴
typ ┴ ┴ └┘ └┘ ┴ ┴
doc └──┘ ┴ └┘ └┘ ┴
885 by rw [coeff_X, if_pos rfl]
886
887 lemma X_pow_eq (n : ℕ) : (X : power_series α)^n = monomial α n 1 :=
id ┴ └┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ └┘ └┘ ┴
typ ┴ └┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘ └┘ ┴
888 mv_power_series.X_pow_eq _ n
id ┴
typ ┴
889
890 lemma coeff_X_pow (m n : ℕ) :
id ┴
src ┴
typ ┴
891 coeff α m ((X : power_series α)^n) = if m = n then 1 else 0 :=
id ┴ ┴ └┘ └┘ └┘ ┴ ┴ ┴ ┴
src └┘ └┘ └┘
typ ┴ ┴ └┘ └┘ └┘ ┴ ┴ ┴ ┴
doc └┘ └┘ └┘
892 by rw [X_pow_eq, coeff_monomial]
st ┴
893
894 @[simp] lemma coeff_X_pow_self (n : ℕ) :
id ┴
src ┴
typ ┴
doc └──┘
895 coeff α n ((X : power_series α)^n) = 1 :=
id ┴ ┴ └┘ └┘ └┘ ┴ ┴
src └┘ └┘ └┘
typ ┴ ┴ └┘ └┘ └┘ ┴ ┴
doc └┘ └┘ └┘
896 by rw [coeff_X_pow, if_pos rfl]
897
898 @[simp] lemma coeff_one (n : ℕ) :
id ┴
src ┴
typ ┴
doc └──┘
899 coeff α n (1 : power_series α) = if n = 0 then 1 else 0 :=
id ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴
src ┴ └┘ └┘ ┴
typ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴
doc ┴ └┘ └┘ ┴
900 calc coeff α n (1 : power_series α) = _ : mv_power_series.coeff_one _
id ┴ ┴ └┘ └┘ └┘
src └┘ └┘ └┘
typ ┴ ┴ └┘ └┘ └┘
doc └┘ └┘ └┘
901 ... = if n = 0 then 1 else 0 :
id ┴
typ ┴
902 by { simp only [finsupp.single_eq_zero], split_ifs; refl }
id └──┘
src └──┘
typ └──┘
doc └──┘
st └┘
903
904 @[simp] lemma coeff_zero_one : coeff α 0 (1 : power_series α) = 1 :=
id ┴ ┴ └┘ └┘ ┴ ┴
src ┴ └┘ └┘ ┴
typ ┴ ┴ └┘ └┘ ┴ ┴
doc └──┘ ┴ └┘ └┘ ┴
905 coeff_zero_C 1
906
907 lemma coeff_mul (n : ℕ) (φ ψ : power_series α) :
id ┴ ┴
src ┴
typ ┴ ┴
908 coeff α n (φ * ψ) = (finset.nat.antidiagonal n).sum (λ p, coeff α p.1 φ * coeff α p.2 ψ) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
909 begin
910 symmetry,
911 apply finset.sum_bij (λ (p : ℕ × ℕ) h, (single () p.1, single () p.2)),
912 { rintros ⟨i,j⟩ hij, rw finset.nat.mem_antidiagonal at hij,
913 rw [finsupp.mem_antidiagonal_support, ← finsupp.single_add, hij], },
st ┴ └┘
914 { rintros ⟨i,j⟩ hij, refl },
st └┘
915 { rintros ⟨i,j⟩ ⟨k,l⟩ hij hkl,
916 simpa only [prod.mk.inj_iff, finsupp.unique_single_eq_iff] using id },
st └┘
917 { rintros ⟨f,g⟩ hfg,
918 refine ⟨(f (), g ()), _, _⟩,
id ┴ ┴
typ ┴ ┴
919 { rw finsupp.mem_antidiagonal_support at hfg,
920 rw [finset.nat.mem_antidiagonal, ← finsupp.add_apply, hfg, finsupp.single_eq_same] },
st ┴ └┘
921 { rw prod.mk.inj_iff, dsimp,
922 exact ⟨finsupp.unique_single f, finsupp.unique_single g⟩ } }
id ┴ ┴
typ ┴ ┴
st └───
923 end
st ──┘
924
925 @[simp] lemma coeff_mul_C (n : ℕ) (φ : power_series α) (a : α) :
id ┴ └┘ └┘ └┘ ┴ ┴
src ┴ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴ ┴
doc └──┘ └┘ └┘ └┘
926 coeff α n (φ * (C α a)) = (coeff α n φ) * a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
927 mv_power_series.coeff_mul_C _ φ a
id ┴ ┴
typ ┴ ┴
928
929 @[simp] lemma coeff_succ_mul_X (n : ℕ) (φ : power_series α) :
id ┴ └┘ └┘ └┘ ┴
src ┴ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴
doc └──┘ └┘ └┘ └┘
930 coeff α (n+1) (φ * X) = coeff α n φ :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
931 begin
932 rw [coeff_mul _ φ, finset.sum_eq_single (n,1)],
933 { rw [coeff_X, if_pos rfl, mul_one] },
st ┴ └┘
934 { rintro ⟨i,j⟩ hij hne,
935 by_cases hj : j = 1,
id ┴
typ ┴
936 { subst hj, simp at *, contradiction },
st └┘
937 { simp [coeff_X, hj] } },
st └──┘
938 { intro h, exfalso, apply h, simp },
st └┘
939 end
st └─┘
940
941 @[simp] lemma coeff_zero_mul_X (φ : power_series α) :
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └──┘ └┘ └┘ └┘
942 coeff α 0 (φ * X) = 0 :=
id ┴ ┴
typ ┴ ┴
943 begin
944 rw [coeff_mul _ φ, finset.sum_eq_zero],
945 rintro ⟨i,j⟩ hij,
946 obtain ⟨rfl, rfl⟩ : i = 0 ∧ j = 0, { simpa using hij },
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
st └┘
947 simp,
948 end
st └─┘
949
950 @[simp] lemma constant_coeff_C (a : α) : constant_coeff α (C α a) = a := rfl
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
951 @[simp] lemma constant_coeff_comp_C :
doc └──┘
952 (constant_coeff α).comp (C α) = ring_hom.id α := rfl
id ┴ ┴ ┴
typ ┴ ┴ ┴
953
954 @[simp] lemma constant_coeff_zero : constant_coeff α 0 = 0 := rfl
id ┴
typ ┴
doc └──┘
955 @[simp] lemma constant_coeff_one : constant_coeff α 1 = 1 := rfl
id ┴
typ ┴
doc └──┘
956 @[simp] lemma constant_coeff_X : constant_coeff α X = 0 := mv_power_series.coeff_zero_X _
id ┴
typ ┴
doc └──┘
957
958 /-- If a formal power series is invertible, then so is its constant coefficient.-/
959 lemma is_unit_constant_coeff (φ : power_series α) (h : is_unit φ) :
id └┘ └┘ └┘ ┴ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴
doc └┘ └┘ └┘
960 is_unit (constant_coeff α φ) :=
id ┴ ┴
typ ┴ ┴
961 mv_power_series.is_unit_constant_coeff φ h
id ┴
typ ┴
962
963 section map
964 variables {β : Type*} {γ : Type*} [semiring β] [semiring γ]
id ┴ └┘ ┴ └─┘ └─┘
src ┴ └┘ ┴ └─┘ └─┘
typ ┴ └┘ ┴ └─┘ └─┘
965 variables (f : α →+* β) (g : β →+* γ)
966
967 /-- The map between formal power series induced by a map on the coefficients.-/
968 def map : power_series α →+* power_series β :=
id └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴
src └┘ └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘ └┘ └┘ └┘
969 mv_power_series.map _ f
970
971 @[simp] lemma map_id : (map (ring_hom.id α) :
id ┴
typ ┴
doc └──┘
972 power_series α → power_series α) = id := rfl
id ┴ └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
973
974 lemma map_comp : map (g.comp f) = (map g).comp (map f) := rfl
975
976 @[simp] lemma coeff_map (n : ℕ) (φ : power_series α) :
id ┴ └─┘ └┘ └┘ ┴
src ┴ └─┘ └┘ └┘
typ ┴ └─┘ └┘ └┘ ┴
doc └──┘ └─┘ └┘ └┘
977 coeff β n (map f φ) = f (coeff α n φ) := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
978
979 end map
980
981 end semiring
982
983 section comm_semiring
984 variables [comm_semiring α]
id ┴ └──┘ └──┘
src ┴ └──┘ └──┘
typ ┴ └──┘ └──┘
985
986 lemma X_pow_dvd_iff {n : ℕ} {φ : power_series α} :
id ┴ └┘ └┘ └┘ ┴
src ┴ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
987 (X : power_series α)^n ∣ φ ↔ ∀ m, m < n → coeff α m φ = 0 :=
id ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ └┘ ┴ ┴
typ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ └┘ └┘ ┴
988 begin
989 convert @mv_power_series.X_pow_dvd_iff unit α _ () n φ, apply propext,
id └──┘ ┴ └┘ ┴ ┴
src └──┘ └┘
typ └──┘ ┴ └┘ ┴ ┴
doc └──┘
990 classical, split; intros h m hm,
991 { rw finsupp.unique_single m, convert h _ hm },
id ┴
typ ┴
st └┘
992 { apply h, simpa only [finsupp.single_eq_same] using hm }
id └┘
typ └┘
st └─
993 end
st ──┘
994
995 lemma X_dvd_iff {φ : power_series α} :
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
996 (X : power_series α) ∣ φ ↔ constant_coeff α φ = 0 :=
id └┘ └┘ └┘ ┴ ┴ ┴ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴ ┴ ┴
doc └┘ └┘ └┘
997 begin
998 rw [← pow_one (X : power_series α), X_pow_dvd_iff, ← coeff_zero_eq_constant_coeff_apply],
999 split; intro h,
1000 { exact h 0 zero_lt_one },
st └┘
1001 { intros m hm, rwa nat.eq_zero_of_le_zero (nat.le_of_succ_le_succ hm) }
st └─
1002 end
st ──┘
1003
1004 section trunc
1005
1006 /-- The `n`th truncation of a formal power series to a polynomial -/
1007 def trunc (n : ℕ) (φ : power_series α) : polynomial α :=
id ┴ └┘ └┘ └┘ ┴ ┴
src ┴ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴ ┴
doc └┘ └┘ └┘
1008 { support := ((finset.nat.antidiagonal n).image prod.fst).filter (λ m, coeff α m φ ≠ 0),
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1009 to_fun := λ m, if m ≤ n then coeff α m φ else 0,
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1010 mem_support_to_fun := λ m,
id ┴
typ ┴
1011 begin
1012 suffices : m ∈ ((finset.nat.antidiagonal n).image prod.fst) ↔ m ≤ n,
id ┴ ┴
typ ┴ ┴
1013 { rw [finset.mem_filter, this], split,
1014 { intro h, rw [if_pos h.1], exact h.2 },
st └┘
1015 { intro h, split_ifs at h with H H,
1016 { exact ⟨H, h⟩ },
id ┴
typ ┴
st └┘
1017 { exfalso, exact h rfl } } },
st └────┘
1018 rw finset.mem_image, split,
1019 { rintros ⟨⟨i,j⟩, h, rfl⟩,
1020 rw finset.nat.mem_antidiagonal at h,
1021 rw ← h, exact nat.le_add_right _ _ },
st └┘
1022 { intro h, refine ⟨(m, n-m), _, rfl⟩,
id ┴ ┴
typ ┴ ┴
1023 rw finset.nat.mem_antidiagonal, exact nat.add_sub_of_le h }
id ┴
typ ┴
st └┘
1024 end }
st └─┘
1025
1026 lemma coeff_trunc (m) (n) (φ : power_series α) :
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
1027 polynomial.coeff (trunc n φ) m = if m ≤ n then coeff α m φ else 0 := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1028
1029 @[simp] lemma trunc_zero (n) : trunc n (0 : power_series α) = 0 :=
id ┴ └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴
doc └──┘ └┘ └┘ └┘
1030 polynomial.ext $ λ m,
id ┴
typ ┴
1031 begin
1032 rw [coeff_trunc, add_monoid_hom.map_zero, polynomial.coeff_zero],
1033 split_ifs; refl
id └──┘
src └──┘
typ └──┘
doc └──┘
1034 end
st └─┘
1035
1036 @[simp] lemma trunc_one (n) : trunc n (1 : power_series α) = 1 :=
id ┴ └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴
doc └──┘ └┘ └┘ └┘
1037 polynomial.ext $ λ m,
id ┴
typ ┴
1038 begin
1039 rw [coeff_trunc, coeff_one],
1040 split_ifs with H H' H'; rw [polynomial.coeff_one],
1041 { subst m, rw [if_pos rfl] },
id ┴
typ ┴
st ┴ └┘
1042 { symmetry, exact if_neg (ne.elim (ne.symm H')) },
st └┘
1043 { symmetry, refine if_neg _,
1044 intro H', apply H, subst m, exact nat.zero_le _ }
id ┴
typ ┴
st └─
1045 end
st ──┘
1046
1047 @[simp] lemma trunc_C (n) (a : α) : trunc n (C α a) = polynomial.C a :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
1048 polynomial.ext $ λ m,
id ┴
typ ┴
1049
1050 begin
1051 rw [coeff_trunc, coeff_C, polynomial.coeff_C],
1052 split_ifs with H; refl <|> try {simp * at *}
id └──┘ └─┘
src └──┘ └─┘
typ └──┘ └─┘
doc └──┘ └─┘
st └─
1053 end
st ──┘
1054
1055 @[simp] lemma trunc_add (n) (φ ψ : power_series α) :
id ┴
typ ┴
doc └──┘
1056 trunc n (φ + ψ) = trunc n φ + trunc n ψ :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1057 polynomial.ext $ λ m,
id ┴
typ ┴
1058 begin
1059 simp only [coeff_trunc, add_monoid_hom.map_add, polynomial.coeff_add],
1060 split_ifs with H, {refl}, {rw [zero_add]}
st └┘ └──
1061 end
st ──┘
1062
1063 end trunc
1064
1065 end comm_semiring
1066
1067 section ring
1068 variables [ring α]
id └┘
src └┘
typ └┘
1069
1070 protected def inv.aux : α → power_series α → power_series α :=
id ┴ ┴ └─┘ └┘ └┘ ┴
src └─┘ └┘ └┘
typ ┴ ┴ └─┘ └┘ └┘ ┴
doc └─┘ └┘ └┘
1071 mv_power_series.inv.aux
1072
1073 lemma coeff_inv_aux (n : ℕ) (a : α) (φ : power_series α) :
id ┴ ┴ └┘ └┘ └┘ ┴
src ┴ └┘ └┘ └┘
typ ┴ ┴ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
1074 coeff α n (inv.aux a φ) = if n = 0 then a else
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1075 - a * (finset.nat.antidiagonal n).sum (λ (x : ℕ × ℕ),
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
1076 if x.2 < n then coeff α x.1 φ * coeff α x.2 (inv.aux a φ) else 0) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1077 begin
1078 rw [coeff, inv.aux, mv_power_series.coeff_inv_aux],
1079 simp only [finsupp.single_eq_zero],
1080 split_ifs, {refl},
st └┘
1081 congr' 1,
1082 symmetry,
1083 apply finset.sum_bij (λ (p : ℕ × ℕ) h, (single () p.1, single () p.2)),
id └┘
src └┘
typ └┘
1084 { rintros ⟨i,j⟩ hij, rw finset.nat.mem_antidiagonal at hij,
1085 rw [finsupp.mem_antidiagonal_support, ← finsupp.single_add, hij], },
st ┴ └┘
1086 { rintros ⟨i,j⟩ hij,
1087 by_cases H : j < n,
id ┴ ┴
typ ┴ ┴
1088 { rw [if_pos H, if_pos], {refl},
id ┴
typ ┴
st └┘
1089 split,
1090 { rintro ⟨⟩, simpa [finsupp.single_eq_same] using le_of_lt H },
id ┴
typ ┴
st └┘
1091 { intro hh, rw lt_iff_not_ge at H, apply H,
1092 simpa [finsupp.single_eq_same] using hh () } },
id └┘
src └┘
typ └┘
st └──┘
1093 { rw [if_neg H, if_neg], rintro ⟨h₁, h₂⟩, apply h₂, rintro ⟨⟩,
id ┴
typ ┴
1094 simpa [finsupp.single_eq_same] using not_lt.1 H } },
st └──┘
1095 { rintros ⟨i,j⟩ ⟨k,l⟩ hij hkl,
1096 simpa only [prod.mk.inj_iff, finsupp.unique_single_eq_iff] using id },
st └┘
1097 { rintros ⟨f,g⟩ hfg,
1098 refine ⟨(f (), g ()), _, _⟩,
id ┴ ┴
typ ┴ ┴
1099 { rw finsupp.mem_antidiagonal_support at hfg,
1100 rw [finset.nat.mem_antidiagonal, ← finsupp.add_apply, hfg, finsupp.single_eq_same] },
st ┴ └┘
1101 { rw prod.mk.inj_iff, dsimp,
1102 exact ⟨finsupp.unique_single f, finsupp.unique_single g⟩ } }
id ┴ ┴
typ ┴ ┴
st └───
1103 end
st ──┘
1104
1105 /-- A formal power series is invertible if the constant coefficient is invertible.-/
1106 def inv_of_unit (φ : power_series α) (u : units α) : power_series α :=
id └┘ └┘ └┘ ┴ ┴ └┘ └┘ └┘ ┴
src └┘ └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘ └┘ └┘ └┘
1107 mv_power_series.inv_of_unit φ u
id ┴
typ ┴
1108
1109 lemma coeff_inv_of_unit (n : ℕ) (φ : power_series α) (u : units α) :
id ┴ └┘ └┘ └┘ ┴ ┴
src ┴ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴ ┴
doc └┘ └┘ └┘
1110 coeff α n (inv_of_unit φ u) = if n = 0 then ↑u⁻¹ else
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1111 - ↑u⁻¹ * (finset.nat.antidiagonal n).sum (λ (x : ℕ × ℕ),
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
1112 if x.2 < n then coeff α x.1 φ * coeff α x.2 (inv_of_unit φ u) else 0) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1113 coeff_inv_aux n ↑u⁻¹ φ
id ┴ ┴
typ ┴ ┴
1114
1115 @[simp] lemma constant_coeff_inv_of_unit (φ : power_series α) (u : units α) :
id └┘ └┘ └┘ ┴ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴
doc └──┘ └┘ └┘ └┘
1116 constant_coeff α (inv_of_unit φ u) = ↑u⁻¹ :=
id ┴ ┴
typ ┴ ┴
1117 by rw [← coeff_zero_eq_constant_coeff_apply, coeff_inv_of_unit, if_pos rfl]
st ┴
1118
1119 lemma mul_inv_of_unit (φ : power_series α) (u : units α) (h : constant_coeff α φ = u) :
id └┘ └┘ └┘ ┴ ┴ ┴ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴ ┴ ┴
doc └┘ └┘ └┘
1120 φ * inv_of_unit φ u = 1 :=
id ┴ ┴
typ ┴ ┴
1121 mv_power_series.mul_inv_of_unit φ u $ h
id ┴
typ ┴
1122
1123 end ring
1124
1125 section integral_domain
1126 variable [integral_domain α]
id └┘ └┘ └┘ └┘ └┘
src └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ └┘
1127
1128 lemma eq_zero_or_eq_zero_of_mul_eq_zero (φ ψ : power_series α) (h : φ * ψ = 0) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
1129 φ = 0 ∨ ψ = 0 :=
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
1130 begin
1131 rw classical.or_iff_not_imp_left, intro H,
1132 have ex : ∃ m, coeff α m φ ≠ 0, { contrapose! H, exact ext H },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
1133 let P : ℕ → Prop := λ k, coeff α k φ ≠ 0,
id ┴ ┴ ┴
typ ┴ ┴ ┴
1134 let m := nat.find ex,
1135 have hm₁ : coeff α m φ ≠ 0 := nat.find_spec ex,
id ┴ ┴ ┴
typ ┴ ┴ ┴
1136 have hm₂ : ∀ k < m, ¬coeff α k φ ≠ 0 := λ k, nat.find_min ex,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1137 ext n, rw (coeff α n).map_zero, apply nat.strong_induction_on n,
id ┴ ┴ ┴
typ ┴ ┴ ┴
1138 clear n, intros n ih,
1139 replace h := congr_arg (coeff α (m + n)) h,
id ┴ ┴ ┴
typ ┴ ┴ ┴
1140 rw [add_monoid_hom.map_zero, coeff_mul, finset.sum_eq_single (m,n)] at h,
id ┴ ┴
typ ┴ ┴
1141 { replace h := eq_zero_or_eq_zero_of_mul_eq_zero h,
1142 rw or_iff_not_imp_left at h, exact h hm₁ },
st └┘
1143 { rintro ⟨i,j⟩ hij hne,
1144 by_cases hj : j < n, { rw [ih j hj, mul_zero] },
id ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ └┘
st ┴ └┘
1145 by_cases hi : i < m,
id ┴ ┴
typ ┴ ┴
1146 { specialize hm₂ _ hi, push_neg at hm₂, rw [hm₂, zero_mul] },
id └┘
typ └┘
st ┴ └┘
1147 rw finset.nat.mem_antidiagonal at hij,
1148 push_neg at hi hj,
1149 suffices : m < i,
id ┴ ┴
typ ┴ ┴
1150 { have : m + n < i + j := add_lt_add_of_lt_of_le this hj,
id ┴ ┴ ┴ ┴ └──┘ └┘
typ ┴ ┴ ┴ ┴ └──┘ └┘
1151 exfalso, exact ne_of_lt this hij.symm },
st └┘
1152 contrapose! hne, have : i = m := le_antisymm hne hi, subst i, clear hi hne,
id ┴ ┴ └─┘ └┘ ┴
typ ┴ ┴ └─┘ └┘ ┴
1153 simpa [ne.def, prod.mk.inj_iff] using (add_left_inj m).mp hij },
id ┴
typ ┴
st └┘
1154 { contrapose!, intro h, rw finset.nat.mem_antidiagonal }
st └─
1155 end
st ──┘
1156
1157 instance : integral_domain (power_series α) :=
id └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴
src └┘ └┘ └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
1158 { eq_zero_or_eq_zero_of_mul_eq_zero := eq_zero_or_eq_zero_of_mul_eq_zero,
1159 .. power_series.nonzero_comm_ring }
1160
1161 /-- The ideal spanned by the variable in the power series ring
1162 over an integral domain is a prime ideal.-/
1163 lemma span_X_is_prime : (ideal.span ({X} : set (power_series α))).is_prime :=
id └┘ └┘ └┘ └┘ ┴
src └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
1164 begin
1165 suffices : ideal.span ({X} : set (power_series α)) = is_ring_hom.ker (constant_coeff α),
id └─┘ └──────────┘ ┴
src └─┘ └──────────┘
typ └─┘ └──────────┘ ┴
doc └──────────┘
1166 { rw this, exact is_ring_hom.ker_is_prime _ },
st └┘
1167 apply ideal.ext, intro φ,
1168 rw [is_ring_hom.mem_ker, ideal.mem_span_singleton, X_dvd_iff]
st ┴
1169 end
st └─┘
1170
1171 /-- The variable of the power series ring over an integral domain is prime.-/
1172 lemma X_prime : prime (X : power_series α) :=
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
1173 begin
1174 rw ← ideal.span_singleton_prime,
1175 { exact span_X_is_prime },
st └┘
1176 { intro h, simpa using congr_arg (coeff α 1) h }
id ┴
typ ┴
st └─
1177 end
st ──┘
1178
1179 end integral_domain
1180
1181 section local_ring
1182 variables [comm_ring α]
id └┘ └──┘
src └┘ └──┘
typ └┘ └──┘
1183
1184 lemma is_local_ring (h : is_local_ring α) :
id ┴
typ ┴
1185 is_local_ring (power_series α) :=
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
1186 mv_power_series.is_local_ring h
id ┴
typ ┴
1187
1188 end local_ring
1189
1190 section local_ring
1191 variables {β : Type*} [local_ring α] [local_ring β] (f : α →+* β) [is_local_ring_hom f]
id └──┘ └─┘ └─┘ └──┘
src └──┘ └─┘ └─┘ └──┘
typ └──┘ └─┘ └─┘ └──┘
1192
1193 instance : local_ring (power_series α) :=
id └┘ └┘ └┘ └┘ └┘ └┘ ┴
src └┘ └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
1194 mv_power_series.local_ring
1195
1196 instance map.is_local_ring_hom :
1197 is_local_ring_hom (map f) :=
1198 mv_power_series.map.is_local_ring_hom f
1199
1200 end local_ring
1201
1202 section discrete_field
1203 variables [discrete_field α]
id └┘ └──┘ └──┘
src └┘ └──┘ └──┘
typ └┘ └──┘ └──┘
1204
1205 protected def inv : power_series α → power_series α :=
id ┴ └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
1206 mv_power_series.inv
1207
1208 instance : has_inv (power_series α) := ⟨power_series.inv⟩
id └┘ ┴ ┴ └┘ └┘ ┴ ┴
src └┘ ┴ ┴ └┘ └┘ ┴
typ └┘ ┴ ┴ └┘ └┘ ┴ ┴
doc ┴ └┘ └┘ ┴
1209
1210 lemma inv_eq_inv_aux (φ : power_series α) :
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
1211 φ⁻¹ = inv.aux (constant_coeff α φ)⁻¹ φ := rfl
id ┴ ┴ ┴
typ ┴ ┴ ┴
1212
1213 lemma coeff_inv (n) (φ : power_series α) :
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
1214 coeff α n (φ⁻¹) = if n = 0 then (constant_coeff α φ)⁻¹ else
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1215 - (constant_coeff α φ)⁻¹ * (finset.nat.antidiagonal n).sum (λ (x : ℕ × ℕ),
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1216 if x.2 < n then coeff α x.1 φ * coeff α x.2 (φ⁻¹) else 0) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1217 by rw [inv_eq_inv_aux, coeff_inv_aux n (constant_coeff α φ)⁻¹ φ]
id ┴ ┴ ┴
typ ┴ ┴ ┴
st ┴
1218
1219 @[simp] lemma constant_coeff_inv (φ : power_series α) :
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └──┘ └┘ └┘ └┘
1220 constant_coeff α (φ⁻¹) = (constant_coeff α φ)⁻¹ :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1221 mv_power_series.constant_coeff_inv φ
id ┴
typ ┴
1222
1223 lemma inv_eq_zero {φ : power_series α} :
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
1224 φ⁻¹ = 0 ↔ constant_coeff α φ = 0 :=
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
1225 mv_power_series.inv_eq_zero
1226
1227 @[simp] lemma inv_of_unit_eq (φ : power_series α) (h : constant_coeff α φ ≠ 0) :
id └┘ └┘ └┘ ┴ ┴ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴ ┴
doc └──┘ └┘ └┘ └┘
1228 inv_of_unit φ (units.mk0 _ h) = φ⁻¹ :=
id ┴ ┴
typ ┴ ┴
1229 mv_power_series.inv_of_unit_eq _ _
1230
1231 @[simp] lemma inv_of_unit_eq' (φ : power_series α) (u : units α) (h : constant_coeff α φ = u) :
id └┘ └┘ └┘ ┴ ┴ ┴ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴ ┴ ┴
doc └──┘ └┘ └┘ └┘
1232 inv_of_unit φ u = φ⁻¹ :=
id ┴ ┴
typ ┴ ┴
1233 mv_power_series.inv_of_unit_eq' φ _ h
id ┴
typ ┴
1234
1235 @[simp] protected lemma mul_inv (φ : power_series α) (h : constant_coeff α φ ≠ 0) :
id ┴ └┘ └┘ ┴ ┴ ┴ ┴
src ┴ └┘ └┘ ┴
typ ┴ └┘ └┘ ┴ ┴ ┴ ┴
doc └──┘ ┴ └┘ └┘ ┴
1236 φ * φ⁻¹ = 1 :=
id ┴ ┴
typ ┴ ┴
1237 mv_power_series.mul_inv φ h
id ┴
typ ┴
1238
1239 @[simp] protected lemma inv_mul (φ : power_series α) (h : constant_coeff α φ ≠ 0) :
id └┘ └┘ └┘ ┴ ┴ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴ ┴
doc └──┘ └┘ └┘ └┘
1240 φ⁻¹ * φ = 1 :=
id ┴ ┴
typ ┴ ┴
1241 mv_power_series.inv_mul φ h
id ┴
typ ┴
1242
1243 end discrete_field
1244
1245 end power_series
1246
1247 namespace power_series
1248 variable {α : Type*}
1249
1250 local attribute [instance, priority 1] classical.prop_decidable
1251 noncomputable theory
1252
1253 section order_basic
1254 open multiplicity
1255 variables [comm_semiring α]
id └┘ └──┘ └─┘
src └┘ └──┘ └─┘
typ └┘ └──┘ └─┘
1256
1257 /-- The order of a formal power series `φ` is the smallest `n : enat`
1258 such that `X^n` divides `φ`. The order is `⊤` if and only if `φ = 0`. -/
1259 @[reducible] def order (φ : power_series α) : enat :=
id └┘ └┘ └┘ ┴ ┴ └┘
src └┘ └┘ └┘ ┴ └┘
typ └┘ └┘ └┘ ┴ ┴ └┘
doc └───────┘ └┘ └┘ └┘
1260 multiplicity X φ
id ┴
typ ┴
1261
1262 lemma order_finite_of_coeff_ne_zero (φ : power_series α) (h : ∃ n, coeff α n φ ≠ 0) :
id └┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘ └┘
1263 (order φ).dom :=
id ┴
typ ┴
1264 begin
1265 cases h with n h, refine ⟨n, _⟩,
id ┴
typ ┴
1266 rw X_pow_dvd_iff, push_neg, exact ⟨n, lt_add_one n, h⟩
id ┴
typ ┴
1267 end
st └─┘
1268
1269 /-- If the order of a formal power series is finite,
1270 then the coefficient indexed by the order is nonzero.-/
1271 lemma coeff_order (φ : power_series α) (h : (order φ).dom) :
id └┘ └┘ └┘ ┴ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴
doc └┘ └┘ └┘
1272 coeff α (φ.order.get h) φ ≠ 0 :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
1273 begin
1274 have H := nat.find_spec h, contrapose! H, rw X_pow_dvd_iff,
1275 intros m hm, by_cases Hm : m < nat.find h,
id ┴
typ ┴
1276 { have := nat.find_min h Hm, push_neg at this,
1277 rw X_pow_dvd_iff at this, exact this m (lt_add_one m) },
id ┴
typ ┴
st └┘
1278 have : m = nat.find h, {linarith}, {rwa this}
id ┴
typ ┴
st └┘ └─
1279 end
st ──┘
1280
1281 /-- If the `n`th coefficient of a formal power series is nonzero,
1282 then the order of the power series is less than or equal to `n`.-/
1283 lemma order_le (φ : power_series α) (n : ℕ) (h : coeff α n φ ≠ 0) :
id └┘ └┘ └┘ ┴ ┴ ┴ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴ ┴ ┴
doc └┘ └┘ └┘
1284 order φ ≤ n :=
id ┴ ┴
typ ┴ ┴
1285 begin
1286 have h : ¬ X^(n+1) ∣ φ,
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
1287 { rw X_pow_dvd_iff, push_neg, exact ⟨n, lt_add_one n, h⟩ },
id ┴
typ ┴
st └┘
1288 have : (order φ).dom := ⟨n, h⟩,
id ┴ ┴
typ ┴ ┴
1289 rw [← enat.coe_get this, enat.coe_le_coe],
1290 refine nat.find_min' this h
1291 end
st └─┘
1292
1293 /-- The `n`th coefficient of a formal power series is `0` if `n` is strictly
1294 smaller than the order of the power series.-/
1295 lemma coeff_of_lt_order (φ : power_series α) (n : ℕ) (h: ↑n < order φ) :
id └┘ └┘ └┘ ┴ ┴ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴ ┴
doc └┘ └┘ └┘
1296 coeff α n φ = 0 :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
1297 by { contrapose! h, exact order_le _ _ h }
st └┘
1298
1299 /-- The `0` power series is the unique power series with infinite order.-/
1300 lemma order_eq_top {φ : power_series α} :
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
1301 φ.order = ⊤ ↔ φ = 0 :=
id ┴ ┴
src ┴
typ ┴ ┴
1302 begin
1303 rw eq_top_iff,
1304 split,
1305 { intro h, ext n, specialize h (n+1), rw X_pow_dvd_iff at h, exact h n (lt_add_one _) },
id ┴ ┴
typ ┴ ┴
st └┘
1306 { rintros rfl n, exact dvd_zero _ }
st └─
1307 end
st ──┘
1308
1309 /-- The order of the `0` power series is infinite.-/
1310 @[simp] lemma order_zero : order (0 : power_series α) = ⊤ :=
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └──┘ └┘ └┘ └┘
1311 multiplicity.zero _
1312
1313 /-- The order of a formal power series is at least `n` if
1314 the `i`th coefficient is `0` for all `i < n`.-/
1315 lemma order_ge_nat (φ : power_series α) (n : ℕ) (h : ∀ i < n, coeff α i φ = 0) :
id └┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘ └┘
1316 order φ ≥ n :=
id ┴ ┴
typ ┴ ┴
1317 begin
1318 by_contra H, rw not_le at H,
1319 have : (order φ).dom := enat.dom_of_le_some (le_of_lt H),
id ┴
typ ┴
1320 rw [← enat.coe_get this, enat.coe_lt_coe] at H,
1321 exact coeff_order _ this (h _ H)
1322 end
st └─┘
1323
1324 /-- The order of a formal power series is at least `n` if
1325 the `i`th coefficient is `0` for all `i < n`.-/
1326 lemma order_ge (φ : power_series α) (n : enat) (h : ∀ i : ℕ, ↑i < n → coeff α i φ = 0) :
id └┘ └┘ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ └┘ └┘ └─┘ ┴
typ └┘ └┘ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘ └┘
1327 order φ ≥ n :=
id ┴ ┴
typ ┴ ┴
1328 begin
1329 induction n using enat.cases_on,
1330 { show _ ≤ _, rw [lattice.top_le_iff, order_eq_top],
1331 ext i, exact h _ (enat.coe_lt_top i) },
id ┴
typ ┴
st └┘
1332 { apply order_ge_nat, simpa only [enat.coe_lt_coe] using h }
st └─
1333 end
st ──┘
1334
1335 /-- The order of a formal power series is exactly `n` if the `n`th coefficient is nonzero,
1336 and the `i`th coefficient is `0` for all `i < n`.-/
1337 lemma order_eq_nat {φ : power_series α} {n : ℕ} :
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘
1338 order φ = n ↔ (coeff α n φ ≠ 0) ∧ (∀ i, i < n → coeff α i φ = 0) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1339 begin
1340 simp only [eq_some_iff, X_pow_dvd_iff], push_neg,
1341 split,
1342 { rintros ⟨h₁, m, hm₁, hm₂⟩, refine ⟨_, h₁⟩,
1343 suffices : n = m, { rwa this },
id ┴ ┴
typ ┴ ┴
st └┘
1344 suffices : m ≥ n, { linarith },
id ┴ ┴
typ ┴ ┴
st └┘
1345 contrapose! hm₂, exact h₁ _ hm₂ },
id └─┘
typ └─┘
st └┘
1346 { rintros ⟨h₁, h₂⟩, exact ⟨h₂, n, lt_add_one n, h₁⟩ }
id ┴
typ ┴
st └─
1347 end
st ──┘
1348
1349 /-- The order of a formal power series is exactly `n` if the `n`th coefficient is nonzero,
1350 and the `i`th coefficient is `0` for all `i < n`.-/
1351 lemma order_eq {φ : power_series α} {n : enat} :
id └┘ └┘ └┘ ┴ └─┘
src └┘ └┘ └┘ └─┘
typ └┘ └┘ └┘ ┴ └─┘
doc └┘ └┘ └┘
1352 order φ = n ↔ (∀ i:ℕ, ↑i = n → coeff α i φ ≠ 0) ∧ (∀ i:ℕ, ↑i < n → coeff α i φ = 0) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1353 begin
1354 induction n using enat.cases_on,
id ┴
typ ┴
1355 { rw order_eq_top, split,
1356 { rintro rfl, split; intros,
1357 { exfalso, exact enat.coe_ne_top ‹_› ‹_› },
st └┘
1358 { exact (coeff _ _).map_zero } },
st └──┘
1359 { rintro ⟨h₁, h₂⟩, ext i, exact h₂ i (enat.coe_lt_top i) } },
id ┴
typ ┴
st └──┘
1360 { simpa [enat.coe_inj] using order_eq_nat }
st └─
1361 end
st ──┘
1362
1363 /-- The order of the sum of two formal power series
1364 is at least the minimum of their orders.-/
1365 lemma order_add_ge (φ ψ : power_series α) :
id ┴
typ ┴
1366 order (φ + ψ) ≥ min (order φ) (order ψ) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1367 multiplicity.min_le_multiplicity_add
1368
1369 private lemma order_add_of_order_eq.aux (φ ψ : power_series α)
id ┴
typ ┴
1370 (h : order φ ≠ order ψ) (H : order φ < order ψ) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1371 order (φ + ψ) ≤ order φ ⊓ order ψ :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1372 begin
1373 suffices : order (φ + ψ) = order φ,
id ┴ ┴
typ ┴ ┴
1374 { rw [lattice.le_inf_iff, this], exact ⟨le_refl _, le_of_lt H⟩ },
st └┘
1375 { rw order_eq, split,
1376 { intros i hi, rw [(coeff _ _).map_add, coeff_of_lt_order ψ i (hi.symm ▸ H), add_zero],
id ┴ ┴
typ ┴ ┴
1377 exact (order_eq_nat.1 hi.symm).1 },
st └┘
1378 { intros i hi,
1379 rw [(coeff _ _).map_add, coeff_of_lt_order φ i hi,
id ┴ ┴
typ ┴ ┴
1380 coeff_of_lt_order ψ i (lt_trans hi H), zero_add] } }
id ┴ ┴
typ ┴ ┴
st ┴ └───
1381 end
st ──┘
1382
1383 /-- The order of the sum of two formal power series
1384 is the minimum of their orders if their orders differ.-/
1385 lemma order_add_of_order_eq (φ ψ : power_series α) (h : order φ ≠ order ψ) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
1386 order (φ + ψ) = order φ ⊓ order ψ :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1387 begin
1388 refine le_antisymm _ (order_add_ge _ _),
1389 by_cases H₁ : order φ < order ψ,
id ┴ ┴
typ ┴ ┴
1390 { apply order_add_of_order_eq.aux _ _ h H₁ },
st └┘
1391 by_cases H₂ : order ψ < order φ,
id ┴ ┴
typ ┴ ┴
1392 { simpa only [add_comm, lattice.inf_comm] using order_add_of_order_eq.aux _ _ h.symm H₂ },
st └┘
1393 exfalso, exact h (le_antisymm (not_lt.1 H₂) (not_lt.1 H₁))
1394 end
st └─┘
1395
1396 /-- The order of the product of two formal power series
1397 is at least the sum of their orders.-/
1398 lemma order_mul_ge (φ ψ : power_series α) :
id ┴
typ ┴
1399 order (φ * ψ) ≥ order φ + order ψ :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1400 begin
1401 apply order_ge,
1402 intros n hn, rw [coeff_mul, finset.sum_eq_zero],
1403 rintros ⟨i,j⟩ hij,
1404 by_cases hi : ↑i < order φ,
id ┴ ┴
typ ┴ ┴
1405 { rw [coeff_of_lt_order φ i hi, zero_mul] },
id ┴ ┴
typ ┴ ┴
st ┴ └┘
1406 by_cases hj : ↑j < order ψ,
id ┴ ┴
typ ┴ ┴
1407 { rw [coeff_of_lt_order ψ j hj, mul_zero] },
id ┴ ┴
typ ┴ ┴
st ┴ └┘
1408 rw not_lt at hi hj, rw finset.nat.mem_antidiagonal at hij,
1409 exfalso,
1410 apply ne_of_lt (lt_of_lt_of_le hn $ add_le_add' hi hj),
1411 rw [← enat.coe_add, hij]
st ┴
1412 end
st └─┘
1413
1414 /-- The order of the monomial `a*X^n` is infinite if `a = 0` and `n` otherwise.-/
1415 lemma order_monomial (n : ℕ) (a : α) :
id ┴ ┴
src ┴
typ ┴ ┴
1416 order (monomial α n a) = if a = 0 then ⊤ else n :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1417 begin
1418 split_ifs with h,
1419 { rw [h, order_eq_top, add_monoid_hom.map_zero] },
st ┴ └┘
1420 { rw [order_eq], split; intros i hi,
1421 { rw [enat.coe_inj] at hi, rwa [hi, coeff_monomial'] },
st └┘
1422 { rw [enat.coe_lt_coe] at hi, rw [coeff_monomial, if_neg], exact ne_of_lt hi } }
id └┘
typ └┘
st └───
1423 end
st ──┘
1424
1425 /-- The order of the monomial `a*X^n` is `n` if `a ≠ 0`.-/
1426 lemma order_monomial_of_ne_zero (n : ℕ) (a : α) (h : a ≠ 0) :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
1427 order (monomial α n a) = n :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1428 by rw [order_monomial, if_neg h]
1429
1430 end order_basic
1431
1432 section order_zero_ne_one
1433 variables [nonzero_comm_ring α]
id └┘ └──┘ └──┘ ┴
src └┘ └──┘ └──┘ ┴
typ └┘ └──┘ └──┘ ┴
doc └┘ └──┘ └──┘ ┴
1434
1435 /-- The order of the formal power series `1` is `0`.-/
1436 @[simp] lemma order_one : order (1 : power_series α) = 0 :=
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └──┘ └┘ └┘ └┘
1437 by simpa using order_monomial_of_ne_zero 0 (1:α) one_ne_zero
id ┴
typ ┴
1438
1439 /-- The order of the formal power series `X` is `1`.-/
1440 @[simp] lemma order_X : order (X : power_series α) = 1 :=
id └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ └┘ └┘ └┘ ┴
doc └──┘ └┘ └┘ └┘
1441 order_monomial_of_ne_zero 1 (1:α) one_ne_zero
id ┴
typ ┴
1442
1443 /-- The order of the formal power series `X^n` is `n`.-/
1444 @[simp] lemma order_X_pow (n : ℕ) : order ((X : power_series α)^n) = n :=
id ┴ └┘ └┘ └┘ ┴ ┴ ┴
src ┴ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴ ┴ ┴
doc └──┘ └┘ └┘ └┘
1445 by { rw [X_pow_eq, order_monomial_of_ne_zero], exact one_ne_zero }
st └┘
1446
1447 end order_zero_ne_one
1448
1449 section order_integral_domain
1450 variables [integral_domain α]
id └┘ └──┘ └──┘
src └┘ └──┘ └──┘
typ └┘ └──┘ └──┘
1451
1452 /-- The order of the product of two formal power series over an integral domain
1453 is the sum of their orders.-/
1454 lemma order_mul (φ ψ : power_series α) :
id ┴
typ ┴
1455 order (φ * ψ) = order φ + order ψ :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1456 multiplicity.mul (X_prime)
1457
1458 end order_integral_domain
1459
1460 end power_series
1461
1462 namespace polynomial
1463 open finsupp
1464 variables {σ : Type*} {α : Type*} [comm_semiring α]
id └─┘ └─┘ └─┘ ┴
src └─┘ └─┘ └─┘ ┴
typ └─┘ └─┘ └─┘ ┴
1465
1466 /-- The natural inclusion from polynomials into formal power series.-/
1467 instance coe_to_power_series : has_coe (polynomial α) (power_series α) :=
id ┴ └─┘ └┘ └┘ ┴
src └─┘ └┘ └┘
typ ┴ └─┘ └┘ └┘ ┴
doc └─┘ └┘ └┘
1468 ⟨λ φ, power_series.mk $ λ n, coeff φ n⟩
id ┴ ┴ ┴
typ ┴ ┴ ┴
1469
1470 @[simp, elim_cast] lemma coeff_coe (φ : polynomial α) (n) :
id ┴
typ ┴
doc └──┘ └───────┘
1471 power_series.coeff α n φ = coeff φ n :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1472 congr_arg (coeff φ) (finsupp.single_eq_same)
id ┴
typ ┴
1473
1474 @[reducible] def monomial (n : ℕ) (a : α) : polynomial α := single n a
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
doc └───────┘
1475
1476 @[simp, elim_cast] lemma coe_monomial (n : ℕ) (a : α) :
id ┴ ┴
src ┴
typ ┴ ┴
doc └──┘ └───────┘
1477 (monomial n a : power_series α) = power_series.monomial α n a :=
id ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
src └──────────┘
typ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
doc └──────────┘
1478 power_series.ext $ λ m,
id ┴
typ ┴
1479 begin
1480 rw [coeff_coe, power_series.coeff_monomial],
1481 simp only [@eq_comm _ m n],
id ┴ ┴
typ ┴ ┴
1482 convert finsupp.single_apply,
1483 end
st └─┘
1484
1485 @[simp, elim_cast] lemma coe_zero : ((0 : polynomial α) : power_series α) = 0 := rfl
id ┴ └──────────┘ ┴
src └──────────┘
typ ┴ └──────────┘ ┴
doc └──┘ └───────┘ └──────────┘
1486
1487 @[simp, elim_cast] lemma coe_one : ((1 : polynomial α) : power_series α) = 1 :=
id ┴ └──────────┘ ┴
src └──────────┘
typ ┴ └──────────┘ ┴
doc └──┘ └───────┘ └──────────┘
1488 begin
1489 have := coe_monomial 0 (1:α),
id ┴
typ ┴
1490 rwa power_series.monomial_zero_eq_C_apply at this,
1491 end
st └─┘
1492
1493 @[simp, elim_cast] lemma coe_add (φ ψ : polynomial α) :
id ┴
typ ┴
doc └──┘ └───────┘
1494 ((φ + ψ : polynomial α) : power_series α) = φ + ψ := rfl
id ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘
typ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘
1495
1496 @[simp, elim_cast] lemma coe_mul (φ ψ : polynomial α) :
id ┴
typ ┴
doc └──┘ └───────┘
1497 ((φ * ψ : polynomial α) : power_series α) = φ * ψ :=
id ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘
typ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘
1498 power_series.ext $ λ n,
id ┴
typ ┴
1499 by simp only [coeff_coe, power_series.coeff_mul, coeff_mul]
1500
1501 @[simp, elim_cast] lemma coe_C (a : α) :
id ┴
typ ┴
doc └──┘ └───────┘
1502 ((C a : polynomial α) : power_series α) = power_series.C α a :=
id ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘
typ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘
1503 begin
1504 have := coe_monomial 0 a,
id ┴
typ ┴
1505 rwa power_series.monomial_zero_eq_C_apply at this,
1506 end
st └─┘
1507
1508 @[simp, elim_cast] lemma coe_X :
doc └──┘ └───────┘
1509 ((X : polynomial α) : power_series α) = power_series.X :=
id ┴ └──────────┘ ┴
src └──────────┘
typ ┴ └──────────┘ ┴
doc └──────────┘
1510 coe_monomial _ _
1511
1512 namespace coe_to_mv_power_series
1513
1514 instance : is_semiring_hom (coe : polynomial α → power_series α) :=
id ┴ └─┘ └┘ └┘ ┴
src └─┘ └┘ └┘
typ ┴ └─┘ └┘ └┘ ┴
doc └─┘ └┘ └┘
1515 { map_zero := coe_zero,
1516 map_one := coe_one,
1517 map_add := coe_add,
1518 map_mul := coe_mul }
1519
1520 end coe_to_mv_power_series
1521 end polynomial